[STATEMENT]
lemma gauss_eq_0:
  \<open>z = 0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z = 0) = ((Re z)\<^sup>2 + (Im z)\<^sup>2 = 0)
[PROOF STEP]
by (simp add: gauss_eq_iff sum_power2_eq_zero_iff)