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\in ℂ$$
	binom2.2	$$⊢B\in ℂ$$
Assertion	sqeqori	$$⊢A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		binom2.1	$$⊢A\in ℂ$$
2		binom2.2	$$⊢B\in ℂ$$
3	1 2	subsqi	$$⊢A^2-B^2=\left(A+B\right)\left(A-B\right)$$
4	3	eqeq1i	$$⊢A^2-B^2=0\leftrightarrow \left(A+B\right)\left(A-B\right)=0$$
5	1	sqcli	$$⊢A^2\in ℂ$$
6	2	sqcli	$$⊢B^2\in ℂ$$
7	5 6	subeq0i	$$⊢A^2-B^2=0\leftrightarrow A^2=B^2$$
8	1 2	addcli	$$⊢A+B\in ℂ$$
9	1 2	subcli	$$⊢A-B\in ℂ$$
10	8 9	mul0ori	$$⊢\left(A+B\right)\left(A-B\right)=0\leftrightarrow \left(A+B=0\vee A-B=0\right)$$
11	4 7 10	3bitr3i	$$⊢A^2=B^2\leftrightarrow \left(A+B=0\vee A-B=0\right)$$
12		orcom	$$⊢\left(A+B=0\vee A-B=0\right)\leftrightarrow \left(A-B=0\vee A+B=0\right)$$
13	1 2	subeq0i	$$⊢A-B=0\leftrightarrow A=B$$
14	1 2	subnegi	$$⊢A-\left(-B\right)=A+B$$
15	14	eqeq1i	$$⊢A-\left(-B\right)=0\leftrightarrow A+B=0$$
16	2	negcli	$$⊢-B\in ℂ$$
17	1 16	subeq0i	$$⊢A-\left(-B\right)=0\leftrightarrow A=-B$$
18	15 17	bitr3i	$$⊢A+B=0\leftrightarrow A=-B$$
19	13 18	orbi12i	$$⊢\left(A-B=0\vee A+B=0\right)\leftrightarrow \left(A=B\vee A=-B\right)$$
20	11 12 19	3bitri	$$⊢A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)$$