Proof of Theorem pythagtriplem16
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pythagtriplem15.1 | . . . . 5
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) | 
| 2 |  | pythagtriplem15.2 | . . . . 5
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) | 
| 3 | 1, 2 | oveq12i 7444 | . . . 4
⊢ (𝑀 · 𝑁) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) | 
| 4 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℂ) | 
| 5 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) | 
| 6 |  | addcl 11238 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 + 𝐵) ∈ ℂ) | 
| 7 | 4, 5, 6 | syl2anr 597 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℂ) | 
| 8 | 7 | sqrtcld 15477 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 + 𝐵)) ∈
ℂ) | 
| 9 |  | subcl 11508 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 − 𝐵) ∈ ℂ) | 
| 10 | 4, 5, 9 | syl2anr 597 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℂ) | 
| 11 | 10 | sqrtcld 15477 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 −
𝐵)) ∈
ℂ) | 
| 12 |  | addcl 11238 | . . . . . . . . . 10
⊢
(((√‘(𝐶
+ 𝐵)) ∈ ℂ ∧
(√‘(𝐶 −
𝐵)) ∈ ℂ) →
((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 13 | 8, 11, 12 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 14 | 13 | 3adant1 1130 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 15 | 14 | 3ad2ant1 1133 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 16 |  | subcl 11508 | . . . . . . . . . 10
⊢
(((√‘(𝐶
+ 𝐵)) ∈ ℂ ∧
(√‘(𝐶 −
𝐵)) ∈ ℂ) →
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 17 | 8, 11, 16 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 18 | 17 | 3adant1 1130 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 19 | 18 | 3ad2ant1 1133 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) | 
| 20 |  | 2cnne0 12477 | . . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 21 |  | divmuldiv 11968 | . . . . . . . 8
⊢
(((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) ∈ ℂ ∧
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) ∧ ((2 ∈ ℂ
∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 22 | 20, 20, 21 | mpanr12 705 | . . . . . . 7
⊢
((((√‘(𝐶
+ 𝐵)) +
(√‘(𝐶 −
𝐵))) ∈ ℂ ∧
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 23 | 15, 19, 22 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 24 | 13, 17 | mulcld 11282 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) ∈ ℂ) | 
| 25 | 24 | 3adant1 1130 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) ∈ ℂ) | 
| 26 | 25 | 3ad2ant1 1133 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) ∈ ℂ) | 
| 27 |  | divdiv1 11979 | . . . . . . . 8
⊢
(((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
(((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 28 | 20, 20, 27 | mp3an23 1454 | . . . . . . 7
⊢
((((√‘(𝐶
+ 𝐵)) +
(√‘(𝐶 −
𝐵))) ·
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) ∈ ℂ →
(((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 29 | 26, 28 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / (2 · 2))) | 
| 30 | 23, 29 | eqtr4d 2779 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) = (((((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) / 2)) | 
| 31 |  | nnre 12274 | . . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℝ) | 
| 32 |  | nnre 12274 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) | 
| 33 |  | readdcl 11239 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 + 𝐵) ∈ ℝ) | 
| 34 | 31, 32, 33 | syl2anr 597 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ) | 
| 35 | 34 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ) | 
| 36 | 35 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℝ) | 
| 37 | 31 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈
ℝ) | 
| 38 | 32 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈
ℝ) | 
| 39 |  | nngt0 12298 | . . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ ℕ → 0 <
𝐶) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
𝐶) | 
| 41 |  | nngt0 12298 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
𝐵) | 
| 43 | 37, 38, 40, 42 | addgt0d 11839 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
(𝐶 + 𝐵)) | 
| 44 |  | 0re 11264 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ | 
| 45 |  | ltle 11350 | . . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝐶 +
𝐵) ∈ ℝ) →
(0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵))) | 
| 46 | 44, 45 | mpan 690 | . . . . . . . . . . . . 13
⊢ ((𝐶 + 𝐵) ∈ ℝ → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵))) | 
| 47 | 34, 43, 46 | sylc 65 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤
(𝐶 + 𝐵)) | 
| 48 | 47 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤
(𝐶 + 𝐵)) | 
| 49 | 48 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 + 𝐵)) | 
| 50 |  | resqrtth 15295 | . . . . . . . . . 10
⊢ (((𝐶 + 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 + 𝐵)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵)) | 
| 51 | 36, 49, 50 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵)) | 
| 52 |  | resubcl 11574 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 − 𝐵) ∈ ℝ) | 
| 53 | 31, 32, 52 | syl2anr 597 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ) | 
| 54 | 53 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ) | 
| 55 | 54 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ) | 
| 56 |  | pythagtriplem10 16859 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵)) | 
| 57 | 56 | 3adant3 1132 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 < (𝐶 − 𝐵)) | 
| 58 |  | ltle 11350 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (𝐶
− 𝐵) ∈ ℝ)
→ (0 < (𝐶 −
𝐵) → 0 ≤ (𝐶 − 𝐵))) | 
| 59 | 44, 58 | mpan 690 | . . . . . . . . . . 11
⊢ ((𝐶 − 𝐵) ∈ ℝ → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵))) | 
| 60 | 55, 57, 59 | sylc 65 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 − 𝐵)) | 
| 61 |  | resqrtth 15295 | . . . . . . . . . 10
⊢ (((𝐶 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 − 𝐵)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵)) | 
| 62 | 55, 60, 61 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵)) | 
| 63 | 51, 62 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵))↑2) −
((√‘(𝐶 −
𝐵))↑2)) = ((𝐶 + 𝐵) − (𝐶 − 𝐵))) | 
| 64 | 63 | oveq1d 7447 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵))↑2) −
((√‘(𝐶 −
𝐵))↑2)) / 2) =
(((𝐶 + 𝐵) − (𝐶 − 𝐵)) / 2)) | 
| 65 |  | simp12 1204 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℕ) | 
| 66 |  | simp13 1205 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℕ) | 
| 67 | 65, 66, 8 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℂ) | 
| 68 | 65, 66, 11 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℂ) | 
| 69 |  | subsq 14250 | . . . . . . . . 9
⊢
(((√‘(𝐶
+ 𝐵)) ∈ ℂ ∧
(√‘(𝐶 −
𝐵)) ∈ ℂ) →
(((√‘(𝐶 + 𝐵))↑2) −
((√‘(𝐶 −
𝐵))↑2)) =
(((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))))) | 
| 70 | 67, 68, 69 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵))↑2) −
((√‘(𝐶 −
𝐵))↑2)) =
(((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))))) | 
| 71 | 70 | oveq1d 7447 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵))↑2) −
((√‘(𝐶 −
𝐵))↑2)) / 2) =
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2)) | 
| 72 |  | pnncan 11551 | . . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (𝐵 + 𝐵)) | 
| 73 | 72 | 3anidm23 1422 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (𝐵 + 𝐵)) | 
| 74 |  | 2times 12403 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℂ → (2
· 𝐵) = (𝐵 + 𝐵)) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· 𝐵) = (𝐵 + 𝐵)) | 
| 76 | 73, 75 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (2 · 𝐵)) | 
| 77 | 4, 5, 76 | syl2anr 597 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (2 · 𝐵)) | 
| 78 | 77 | 3adant1 1130 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (2 · 𝐵)) | 
| 79 | 78 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) − (𝐶 − 𝐵)) = (2 · 𝐵)) | 
| 80 | 79 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) − (𝐶 − 𝐵)) / 2) = ((2 · 𝐵) / 2)) | 
| 81 |  | 2cn 12342 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 82 |  | 2ne0 12371 | . . . . . . . . . 10
⊢ 2 ≠
0 | 
| 83 |  | divcan3 11949 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝐵) / 2) = 𝐵) | 
| 84 | 81, 82, 83 | mp3an23 1454 | . . . . . . . . 9
⊢ (𝐵 ∈ ℂ → ((2
· 𝐵) / 2) = 𝐵) | 
| 85 | 65, 5, 84 | 3syl 18 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((2 · 𝐵) / 2) = 𝐵) | 
| 86 | 80, 85 | eqtrd 2776 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) − (𝐶 − 𝐵)) / 2) = 𝐵) | 
| 87 | 64, 71, 86 | 3eqtr3d 2784 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) = 𝐵) | 
| 88 | 87 | oveq1d 7447 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) · ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))) / 2) / 2) = (𝐵 / 2)) | 
| 89 | 30, 88 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) + (√‘(𝐶 − 𝐵))) / 2) · (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)) = (𝐵 / 2)) | 
| 90 | 3, 89 | eqtrid 2788 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 · 𝑁) = (𝐵 / 2)) | 
| 91 | 90 | oveq2d 7448 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝑀 · 𝑁)) = (2 · (𝐵 / 2))) | 
| 92 |  | divcan2 11931 | . . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐵 / 2)) = 𝐵) | 
| 93 | 81, 82, 92 | mp3an23 1454 | . . . . 5
⊢ (𝐵 ∈ ℂ → (2
· (𝐵 / 2)) = 𝐵) | 
| 94 | 5, 93 | syl 17 | . . . 4
⊢ (𝐵 ∈ ℕ → (2
· (𝐵 / 2)) = 𝐵) | 
| 95 | 94 | 3ad2ant2 1134 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (2
· (𝐵 / 2)) = 𝐵) | 
| 96 | 95 | 3ad2ant1 1133 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐵 / 2)) = 𝐵) | 
| 97 | 91, 96 | eqtr2d 2777 | 1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 = (2 · (𝑀 · 𝑁))) |