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

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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )