diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 7cfa999..0ebc3fd 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -85,5 +85,30 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
 theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
   Harmonic (Complex.reCLM ∘ f) := by
 
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.reCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-  sorry
+
+theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
+  Harmonic (Complex.imCLM ∘ f) := by
+
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.imCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)