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 ) ↔ ( 𝐴 = 𝐵𝐴 = - 𝐵 ) )