# Metamath Proof Explorer

## 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}↔\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}↔{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}↔if\left({A}\in ℂ,{A},0\right)={B}\right)$
4 eqeq1 ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to \left({A}=-{B}↔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)↔\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}↔\left({A}={B}\vee {A}=-{B}\right)\right)↔\left({if\left({A}\in ℂ,{A},0\right)}^{2}={{B}}^{2}↔\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}↔{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}↔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}↔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)↔\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}↔\left(if\left({A}\in ℂ,{A},0\right)={B}\vee if\left({A}\in ℂ,{A},0\right)=-{B}\right)\right)↔\left({if\left({A}\in ℂ,{A},0\right)}^{2}={if\left({B}\in ℂ,{B},0\right)}^{2}↔\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}↔\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}↔\left({A}={B}\vee {A}=-{B}\right)\right)$