Theorem sqeqori

Description: The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of Gleason p. 311 and its converse. (Contributed by NM, 15-Jan-2006)

	Ref	Expression
Hypotheses	binom2.1	|- A e. CC
	binom2.2	|- B e. CC
Assertion	sqeqori	|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )

Proof

Step	Hyp	Ref	Expression
1		binom2.1	|- A e. CC
2		binom2.2	|- B e. CC
3	1 2	subsqi	|- ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) )
4	3	eqeq1i	|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( ( A + B ) x. ( A - B ) ) = 0 )
5	1	sqcli	|- ( A ^ 2 ) e. CC
6	2	sqcli	|- ( B ^ 2 ) e. CC
7	5 6	subeq0i	|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A ^ 2 ) = ( B ^ 2 ) )
8	1 2	addcli	|- ( A + B ) e. CC
9	1 2	subcli	|- ( A - B ) e. CC
10	8 9	mul0ori	|- ( ( ( A + B ) x. ( A - B ) ) = 0 <-> ( ( A + B ) = 0 \/ ( A - B ) = 0 ) )
11	4 7 10	3bitr3i	|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( ( A + B ) = 0 \/ ( A - B ) = 0 ) )
12		orcom	|- ( ( ( A + B ) = 0 \/ ( A - B ) = 0 ) <-> ( ( A - B ) = 0 \/ ( A + B ) = 0 ) )
13	1 2	subeq0i	|- ( ( A - B ) = 0 <-> A = B )
14	1 2	subnegi	|- ( A - -u B ) = ( A + B )
15	14	eqeq1i	|- ( ( A - -u B ) = 0 <-> ( A + B ) = 0 )
16	2	negcli	|- -u B e. CC
17	1 16	subeq0i	|- ( ( A - -u B ) = 0 <-> A = -u B )
18	15 17	bitr3i	|- ( ( A + B ) = 0 <-> A = -u B )
19	13 18	orbi12i	|- ( ( ( A - B ) = 0 \/ ( A + B ) = 0 ) <-> ( A = B \/ A = -u B ) )
20	11 12 19	3bitri	|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )