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 ⊢ φ → A ∈ ℂ
sqeqd.2 ⊢ φ → B ∈ ℂ
sqeqd.3 ⊢ φ → A 2 = B 2
sqeqd.4 ⊢ φ → 0 ≤ ℜ ⁡ A
sqeqd.5 ⊢ φ → 0 ≤ ℜ ⁡ B
sqeqd.6 ⊢ φ ∧ ℜ ⁡ A = 0 ∧ ℜ ⁡ B = 0 → A = B
Assertion sqeqd ⊢ φ → A = B

Proof

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