Theorem sqeqor

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 Paul Chapman, 15-Mar-2008)

	Ref	Expression
Assertion	sqeqor	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A^2={if\left(A\in ℂ,A,0\right)}^2$$
2	1	eqeq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(A^2=B^2\leftrightarrow {if\left(A\in ℂ,A,0\right)}^2=B^2\right)$$
3		eqeq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(A=B\leftrightarrow if\left(A\in ℂ,A,0\right)=B\right)$$
4		eqeq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(A=-B\leftrightarrow if\left(A\in ℂ,A,0\right)=-B\right)$$
5	3 4	orbi12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(\left(A=B\vee A=-B\right)\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=B\vee if\left(A\in ℂ,A,0\right)=-B\right)\right)$$
6	2 5	bibi12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(\left(A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)\right)\leftrightarrow \left({if\left(A\in ℂ,A,0\right)}^2=B^2\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=B\vee if\left(A\in ℂ,A,0\right)=-B\right)\right)\right)$$
7		oveq1	$$⊢B=if\left(B\in ℂ,B,0\right)\to B^2={if\left(B\in ℂ,B,0\right)}^2$$
8	7	eqeq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left({if\left(A\in ℂ,A,0\right)}^2=B^2\leftrightarrow {if\left(A\in ℂ,A,0\right)}^2={if\left(B\in ℂ,B,0\right)}^2\right)$$
9		eqeq2	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(if\left(A\in ℂ,A,0\right)=B\leftrightarrow if\left(A\in ℂ,A,0\right)=if\left(B\in ℂ,B,0\right)\right)$$
10		negeq	$$⊢B=if\left(B\in ℂ,B,0\right)\to -B=-if\left(B\in ℂ,B,0\right)$$
11	10	eqeq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(if\left(A\in ℂ,A,0\right)=-B\leftrightarrow if\left(A\in ℂ,A,0\right)=-if\left(B\in ℂ,B,0\right)\right)$$
12	9 11	orbi12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left(if\left(A\in ℂ,A,0\right)=B\vee if\left(A\in ℂ,A,0\right)=-B\right)\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=if\left(B\in ℂ,B,0\right)\vee if\left(A\in ℂ,A,0\right)=-if\left(B\in ℂ,B,0\right)\right)\right)$$
13	8 12	bibi12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left({if\left(A\in ℂ,A,0\right)}^2=B^2\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=B\vee if\left(A\in ℂ,A,0\right)=-B\right)\right)\leftrightarrow \left({if\left(A\in ℂ,A,0\right)}^2={if\left(B\in ℂ,B,0\right)}^2\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=if\left(B\in ℂ,B,0\right)\vee if\left(A\in ℂ,A,0\right)=-if\left(B\in ℂ,B,0\right)\right)\right)\right)$$
14		0cn	$$⊢0\in ℂ$$
15	14	elimel	$$⊢if\left(A\in ℂ,A,0\right)\in ℂ$$
16	14	elimel	$$⊢if\left(B\in ℂ,B,0\right)\in ℂ$$
17	15 16	sqeqori	$$⊢{if\left(A\in ℂ,A,0\right)}^2={if\left(B\in ℂ,B,0\right)}^2\leftrightarrow \left(if\left(A\in ℂ,A,0\right)=if\left(B\in ℂ,B,0\right)\vee if\left(A\in ℂ,A,0\right)=-if\left(B\in ℂ,B,0\right)\right)$$
18	6 13 17	dedth2h	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)\right)$$