[STATEMENT]
lemma complex_sqrt_1:
  fixes z::complex
  assumes "z \<noteq> 0"
  shows "z = 1 / z \<longleftrightarrow> z = 1 \<or> z = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
using nonzero_eq_divide_eq square_eq_iff
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
?c \<noteq> (0::?'a) \<Longrightarrow> (?a = ?b / ?c) = (?a * ?c = ?b)
(?a * ?a = ?b * ?b) = (?a = ?b \<or> ?a = - ?b)

goal (1 subgoal):
 1. (z = 1 / z) = (z = 1 \<or> z = - 1)
[PROOF STEP]
by fastforce