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 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 = B 2 ↔ A = B ∨ A = − B

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℂ A 0 → A 2 = if A ∈ ℂ A 0 2
2 1 eqeq1d ⊢ A = if A ∈ ℂ A 0 → A 2 = B 2 ↔ if A ∈ ℂ A 0 2 = B 2
3 eqeq1 ⊢ A = if A ∈ ℂ A 0 → A = B ↔ if A ∈ ℂ A 0 = B
4 eqeq1 ⊢ A = if A ∈ ℂ A 0 → A = − B ↔ if A ∈ ℂ A 0 = − B
5 3 4 orbi12d ⊢ A = if A ∈ ℂ A 0 → A = B ∨ A = − B ↔ if A ∈ ℂ A 0 = B ∨ if A ∈ ℂ A 0 = − B
6 2 5 bibi12d ⊢ A = if A ∈ ℂ A 0 → A 2 = B 2 ↔ A = B ∨ A = − B ↔ if A ∈ ℂ A 0 2 = B 2 ↔ if A ∈ ℂ A 0 = B ∨ if A ∈ ℂ A 0 = − B
7 oveq1 ⊢ B = if B ∈ ℂ B 0 → B 2 = if B ∈ ℂ B 0 2
8 7 eqeq2d ⊢ B = if B ∈ ℂ B 0 → if A ∈ ℂ A 0 2 = B 2 ↔ if A ∈ ℂ A 0 2 = if B ∈ ℂ B 0 2
9 eqeq2 ⊢ B = if B ∈ ℂ B 0 → if A ∈ ℂ A 0 = B ↔ if A ∈ ℂ A 0 = if B ∈ ℂ B 0
10 negeq ⊢ B = if B ∈ ℂ B 0 → − B = − if B ∈ ℂ B 0
11 10 eqeq2d ⊢ B = if B ∈ ℂ B 0 → if A ∈ ℂ A 0 = − B ↔ if A ∈ ℂ A 0 = − if B ∈ ℂ B 0
12 9 11 orbi12d ⊢ B = if B ∈ ℂ B 0 → if A ∈ ℂ A 0 = B ∨ if A ∈ ℂ A 0 = − B ↔ if A ∈ ℂ A 0 = if B ∈ ℂ B 0 ∨ if A ∈ ℂ A 0 = − if B ∈ ℂ B 0
13 8 12 bibi12d ⊢ B = if B ∈ ℂ B 0 → if A ∈ ℂ A 0 2 = B 2 ↔ if A ∈ ℂ A 0 = B ∨ if A ∈ ℂ A 0 = − B ↔ if A ∈ ℂ A 0 2 = if B ∈ ℂ B 0 2 ↔ if A ∈ ℂ A 0 = if B ∈ ℂ B 0 ∨ if A ∈ ℂ A 0 = − if B ∈ ℂ B 0
14 0cn ⊢ 0 ∈ ℂ
15 14 elimel ⊢ if A ∈ ℂ A 0 ∈ ℂ
16 14 elimel ⊢ if B ∈ ℂ B 0 ∈ ℂ
17 15 16 sqeqori ⊢ if A ∈ ℂ A 0 2 = if B ∈ ℂ B 0 2 ↔ if A ∈ ℂ A 0 = if B ∈ ℂ B 0 ∨ if A ∈ ℂ A 0 = − if B ∈ ℂ B 0
18 6 13 17 dedth2h ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 = B 2 ↔ A = B ∨ A = − B