Metamath Proof Explorer

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 ∈ ℂ
binom2.2 ⊢ B ∈ ℂ
Assertion sqeqori ⊢ A 2 = B 2 ↔ A = B ∨ A = − B

Proof

Step Hyp Ref Expression
1 binom2.1 ⊢ A ∈ ℂ
2 binom2.2 ⊢ B ∈ ℂ
3 1 2 subsqi ⊢ A 2 − B 2 = A + B ⁢ A − B
4 3 eqeq1i ⊢ A 2 − B 2 = 0 ↔ A + B ⁢ A − B = 0
5 1 sqcli ⊢ A 2 ∈ ℂ
6 2 sqcli ⊢ B 2 ∈ ℂ
7 5 6 subeq0i ⊢ A 2 − B 2 = 0 ↔ A 2 = B 2
8 1 2 addcli ⊢ A + B ∈ ℂ
9 1 2 subcli ⊢ A − B ∈ ℂ
10 8 9 mul0ori ⊢ A + B ⁢ 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 − − B = A + B
15 14 eqeq1i ⊢ A − − B = 0 ↔ A + B = 0
16 2 negcli ⊢ − B ∈ ℂ
17 1 16 subeq0i ⊢ A − − B = 0 ↔ A = − B
18 15 17 bitr3i ⊢ A + B = 0 ↔ A = − B
19 13 18 orbi12i ⊢ A − B = 0 ∨ A + B = 0 ↔ A = B ∨ A = − B
20 11 12 19 3bitri ⊢ A 2 = B 2 ↔ A = B ∨ A = − B