Metamath Proof Explorer


Theorem sqeqd

Description: A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Hypotheses sqeqd.1 ( 𝜑𝐴 ∈ ℂ )
sqeqd.2 ( 𝜑𝐵 ∈ ℂ )
sqeqd.3 ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
sqeqd.4 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐴 ) )
sqeqd.5 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐵 ) )
sqeqd.6 ( ( 𝜑 ∧ ( ℜ ‘ 𝐴 ) = 0 ∧ ( ℜ ‘ 𝐵 ) = 0 ) → 𝐴 = 𝐵 )
Assertion sqeqd ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 sqeqd.1 ( 𝜑𝐴 ∈ ℂ )
2 sqeqd.2 ( 𝜑𝐵 ∈ ℂ )
3 sqeqd.3 ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
4 sqeqd.4 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐴 ) )
5 sqeqd.5 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐵 ) )
6 sqeqd.6 ( ( 𝜑 ∧ ( ℜ ‘ 𝐴 ) = 0 ∧ ( ℜ ‘ 𝐵 ) = 0 ) → 𝐴 = 𝐵 )
7 sqeqor ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵𝐴 = - 𝐵 ) ) )
8 1 2 7 syl2anc ( 𝜑 → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵𝐴 = - 𝐵 ) ) )
9 3 8 mpbid ( 𝜑 → ( 𝐴 = 𝐵𝐴 = - 𝐵 ) )
10 9 ord ( 𝜑 → ( ¬ 𝐴 = 𝐵𝐴 = - 𝐵 ) )
11 simpl ( ( 𝜑𝐴 = - 𝐵 ) → 𝜑 )
12 fveq2 ( 𝐴 = - 𝐵 → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ - 𝐵 ) )
13 reneg ( 𝐵 ∈ ℂ → ( ℜ ‘ - 𝐵 ) = - ( ℜ ‘ 𝐵 ) )
14 2 13 syl ( 𝜑 → ( ℜ ‘ - 𝐵 ) = - ( ℜ ‘ 𝐵 ) )
15 12 14 sylan9eqr ( ( 𝜑𝐴 = - 𝐵 ) → ( ℜ ‘ 𝐴 ) = - ( ℜ ‘ 𝐵 ) )
16 4 adantr ( ( 𝜑𝐴 = - 𝐵 ) → 0 ≤ ( ℜ ‘ 𝐴 ) )
17 16 15 breqtrd ( ( 𝜑𝐴 = - 𝐵 ) → 0 ≤ - ( ℜ ‘ 𝐵 ) )
18 2 adantr ( ( 𝜑𝐴 = - 𝐵 ) → 𝐵 ∈ ℂ )
19 recl ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
20 18 19 syl ( ( 𝜑𝐴 = - 𝐵 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
21 20 le0neg1d ( ( 𝜑𝐴 = - 𝐵 ) → ( ( ℜ ‘ 𝐵 ) ≤ 0 ↔ 0 ≤ - ( ℜ ‘ 𝐵 ) ) )
22 17 21 mpbird ( ( 𝜑𝐴 = - 𝐵 ) → ( ℜ ‘ 𝐵 ) ≤ 0 )
23 5 adantr ( ( 𝜑𝐴 = - 𝐵 ) → 0 ≤ ( ℜ ‘ 𝐵 ) )
24 0re 0 ∈ ℝ
25 letri3 ( ( ( ℜ ‘ 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ 𝐵 ) = 0 ↔ ( ( ℜ ‘ 𝐵 ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) ) )
26 20 24 25 sylancl ( ( 𝜑𝐴 = - 𝐵 ) → ( ( ℜ ‘ 𝐵 ) = 0 ↔ ( ( ℜ ‘ 𝐵 ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) ) )
27 22 23 26 mpbir2and ( ( 𝜑𝐴 = - 𝐵 ) → ( ℜ ‘ 𝐵 ) = 0 )
28 27 negeqd ( ( 𝜑𝐴 = - 𝐵 ) → - ( ℜ ‘ 𝐵 ) = - 0 )
29 neg0 - 0 = 0
30 28 29 eqtrdi ( ( 𝜑𝐴 = - 𝐵 ) → - ( ℜ ‘ 𝐵 ) = 0 )
31 15 30 eqtrd ( ( 𝜑𝐴 = - 𝐵 ) → ( ℜ ‘ 𝐴 ) = 0 )
32 11 31 27 6 syl3anc ( ( 𝜑𝐴 = - 𝐵 ) → 𝐴 = 𝐵 )
33 32 ex ( 𝜑 → ( 𝐴 = - 𝐵𝐴 = 𝐵 ) )
34 10 33 syld ( 𝜑 → ( ¬ 𝐴 = 𝐵𝐴 = 𝐵 ) )
35 34 pm2.18d ( 𝜑𝐴 = 𝐵 )