This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℂ
binom2.2 ⊢ 𝐵 ∈ ℂ
Assertion sqeqori ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )

Proof

Step Hyp Ref Expression
1 binom2.1 ⊢ 𝐴 ∈ ℂ
2 binom2.2 ⊢ 𝐵 ∈ ℂ
3 1 2 subsqi ⊢ ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) )
4 3 eqeq1i ⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = 0 )
5 1 sqcli ⊢ ( 𝐴 ↑ 2 ) ∈ ℂ
6 2 sqcli ⊢ ( 𝐵 ↑ 2 ) ∈ ℂ
7 5 6 subeq0i ⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
8 1 2 addcli ⊢ ( 𝐴 + 𝐵 ) ∈ ℂ
9 1 2 subcli ⊢ ( 𝐴 − 𝐵 ) ∈ ℂ
10 8 9 mul0ori ⊢ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = 0 ↔ ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) )
11 4 7 10 3bitr3i ⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) )
12 orcom ⊢ ( ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) ↔ ( ( 𝐴 − 𝐵 ) = 0 ∨ ( 𝐴 + 𝐵 ) = 0 ) )
13 1 2 subeq0i ⊢ ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 )
14 1 2 subnegi ⊢ ( 𝐴 − - 𝐵 ) = ( 𝐴 + 𝐵 )
15 14 eqeq1i ⊢ ( ( 𝐴 − - 𝐵 ) = 0 ↔ ( 𝐴 + 𝐵 ) = 0 )
16 2 negcli ⊢ - 𝐵 ∈ ℂ
17 1 16 subeq0i ⊢ ( ( 𝐴 − - 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 )
18 15 17 bitr3i ⊢ ( ( 𝐴 + 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 )
19 13 18 orbi12i ⊢ ( ( ( 𝐴 − 𝐵 ) = 0 ∨ ( 𝐴 + 𝐵 ) = 0 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )
20 11 12 19 3bitri ⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )