Proof of Theorem pythagtriplem14
Step | Hyp | Ref
| Expression |
1 | | pythagtriplem13.1 |
. . 3
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) |
2 | 1 | oveq1i 6559 |
. 2
⊢ (𝑁↑2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵))) /
2)↑2) |
3 | | nncn 10905 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℂ) |
4 | | nncn 10905 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
5 | | addcl 9897 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 + 𝐵) ∈ ℂ) |
6 | 3, 4, 5 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℂ) |
7 | 6 | sqrtcld 14024 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 + 𝐵)) ∈
ℂ) |
8 | | subcl 10159 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 − 𝐵) ∈ ℂ) |
9 | 3, 4, 8 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℂ) |
10 | 9 | sqrtcld 14024 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 −
𝐵)) ∈
ℂ) |
11 | 7, 10 | subcld 10271 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) |
12 | 11 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) |
13 | 12 | 3ad2ant1 1075 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ) |
14 | | 2cn 10968 |
. . . . 5
⊢ 2 ∈
ℂ |
15 | | 2ne0 10990 |
. . . . 5
⊢ 2 ≠
0 |
16 | | sqdiv 12790 |
. . . . 5
⊢
((((√‘(𝐶
+ 𝐵)) −
(√‘(𝐶 −
𝐵))) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2))) |
17 | 14, 15, 16 | mp3an23 1408 |
. . . 4
⊢
(((√‘(𝐶
+ 𝐵)) −
(√‘(𝐶 −
𝐵))) ∈ ℂ →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵))) / 2)↑2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) /
(2↑2))) |
18 | 13, 17 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵))) / 2)↑2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) /
(2↑2))) |
19 | 14 | sqvali 12805 |
. . . . 5
⊢
(2↑2) = (2 · 2) |
20 | 19 | oveq2i 6560 |
. . . 4
⊢
((((√‘(𝐶
+ 𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2↑2))
= ((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2 ·
2)) |
21 | 13 | sqcld 12868 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ) |
22 | | 2cnne0 11119 |
. . . . . . 7
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
23 | | divdiv1 10615 |
. . . . . . 7
⊢
(((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
(((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / 2) / 2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2 ·
2))) |
24 | 22, 22, 23 | mp3an23 1408 |
. . . . . 6
⊢
((((√‘(𝐶
+ 𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) ∈ ℂ
→ (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2 ·
2))) |
25 | 21, 24 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / 2) / 2) =
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2 ·
2))) |
26 | | simp12 1085 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℕ) |
27 | | simp13 1086 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℕ) |
28 | 26, 27, 7 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℂ) |
29 | 26, 27, 10 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℂ) |
30 | | binom2sub 12843 |
. . . . . . . . . 10
⊢
(((√‘(𝐶
+ 𝐵)) ∈ ℂ ∧
(√‘(𝐶 −
𝐵)) ∈ ℂ) →
(((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))))) +
((√‘(𝐶 −
𝐵))↑2))) |
31 | 28, 29, 30 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))))) +
((√‘(𝐶 −
𝐵))↑2))) |
32 | | nnre 10904 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ ℕ → 𝐶 ∈
ℝ) |
33 | | nnre 10904 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
34 | | readdcl 9898 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 + 𝐵) ∈ ℝ) |
35 | 32, 33, 34 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ) |
36 | 35 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℝ) |
38 | 37 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℂ) |
39 | | resubcl 10224 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 − 𝐵) ∈ ℝ) |
40 | 32, 33, 39 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ) |
41 | 40 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ) |
42 | 41 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ) |
43 | 42 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℂ) |
44 | 7 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 + 𝐵)) ∈
ℂ) |
45 | 10 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(√‘(𝐶 −
𝐵)) ∈
ℂ) |
46 | 44, 45 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))) ∈
ℂ) |
47 | | mulcl 9899 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) ∈ ℂ) → (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵)))) ∈
ℂ) |
48 | 14, 46, 47 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (2
· ((√‘(𝐶
+ 𝐵)) ·
(√‘(𝐶 −
𝐵)))) ∈
ℂ) |
49 | 48 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵)))) ∈
ℂ) |
50 | 38, 43, 49 | addsubd 10292 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))))) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵))) |
51 | 27 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℂ) |
52 | | simp11 1084 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℕ) |
53 | 52 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℂ) |
54 | | subdi 10342 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝐶
∈ ℂ ∧ 𝐴
∈ ℂ) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴))) |
55 | 14, 54 | mp3an1 1403 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2
· (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴))) |
56 | 51, 53, 55 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴))) |
57 | | ppncan 10202 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶)) |
58 | 57 | 3anidm13 1376 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶)) |
59 | | 2times 11022 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ ℂ → (2
· 𝐶) = (𝐶 + 𝐶)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· 𝐶) = (𝐶 + 𝐶)) |
61 | 58, 60 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶)) |
62 | 3, 4, 61 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶)) |
63 | 62 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶)) |
64 | 63 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶)) |
65 | 26 | nncnd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℂ) |
66 | | subsq 12834 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵))) |
67 | 51, 65, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵))) |
68 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2))) |
69 | 68 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2))) |
70 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
71 | 70 | sqcld 12868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈
ℂ) |
72 | 71 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈
ℂ) |
73 | 4 | sqcld 12868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈
ℂ) |
74 | 73 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈
ℂ) |
75 | 72, 74 | pncand 10272 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2)) |
76 | 75 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2)) |
77 | 69, 76 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = (𝐴↑2)) |
78 | 67, 77 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) · (𝐶 − 𝐵)) = (𝐴↑2)) |
79 | 78 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = (√‘(𝐴↑2))) |
80 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈
ℝ) |
81 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈
ℝ) |
82 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ ℕ → 0 <
𝐶) |
83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
𝐶) |
84 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
𝐵) |
86 | 80, 81, 83, 85 | addgt0d 10481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 <
(𝐶 + 𝐵)) |
87 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℝ |
88 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ (𝐶 +
𝐵) ∈ ℝ) →
(0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵))) |
89 | 87, 88 | mpan 702 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 + 𝐵) ∈ ℝ → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵))) |
90 | 35, 86, 89 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤
(𝐶 + 𝐵)) |
91 | 90 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤
(𝐶 + 𝐵)) |
92 | 91 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 + 𝐵)) |
93 | | pythagtriplem10 15363 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵)) |
94 | 93 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 < (𝐶 − 𝐵)) |
95 | | ltle 10005 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ (𝐶
− 𝐵) ∈ ℝ)
→ (0 < (𝐶 −
𝐵) → 0 ≤ (𝐶 − 𝐵))) |
96 | 87, 95 | mpan 702 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 − 𝐵) ∈ ℝ → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵))) |
97 | 42, 94, 96 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 − 𝐵)) |
98 | 37, 92, 42, 97 | sqrtmuld 14011 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) |
99 | 79, 98 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐴↑2)) =
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵)))) |
100 | | nnre 10904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
101 | 100 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈
ℝ) |
102 | 101 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℝ) |
103 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
104 | 103 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
105 | 104 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤
𝐴) |
106 | 105 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ 𝐴) |
107 | 102, 106 | sqrtsqd 14006 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐴↑2)) = 𝐴) |
108 | 99, 107 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) = 𝐴) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵)))) = (2 · 𝐴)) |
110 | 64, 109 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))))) = ((2 · 𝐶) − (2 · 𝐴))) |
111 | 56, 110 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵)))))) |
112 | | resqrtth 13844 |
. . . . . . . . . . . . 13
⊢ (((𝐶 + 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 + 𝐵)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵)) |
113 | 37, 92, 112 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵)) |
114 | 113 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵))↑2) − (2 ·
((√‘(𝐶 + 𝐵)) ·
(√‘(𝐶 −
𝐵))))) = ((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))))) |
115 | | resqrtth 13844 |
. . . . . . . . . . . 12
⊢ (((𝐶 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 − 𝐵)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵)) |
116 | 42, 97, 115 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵)) |
117 | 114, 116 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵))↑2) − (2
· ((√‘(𝐶
+ 𝐵)) ·
(√‘(𝐶 −
𝐵))))) +
((√‘(𝐶 −
𝐵))↑2)) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵))) |
118 | 50, 111, 117 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵))↑2) − (2
· ((√‘(𝐶
+ 𝐵)) ·
(√‘(𝐶 −
𝐵))))) +
((√‘(𝐶 −
𝐵))↑2)) = (2 ·
(𝐶 − 𝐴))) |
119 | 31, 118 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = (2 · (𝐶 − 𝐴))) |
120 | 119 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / 2) = ((2
· (𝐶 − 𝐴)) / 2)) |
121 | | subcl 10159 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐶 − 𝐴) ∈ ℂ) |
122 | 3, 70, 121 | syl2anr 494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ) |
123 | 122 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ) |
124 | 123 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐴) ∈ ℂ) |
125 | | divcan3 10590 |
. . . . . . . . 9
⊢ (((𝐶 − 𝐴) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴)) |
126 | 14, 15, 125 | mp3an23 1408 |
. . . . . . . 8
⊢ ((𝐶 − 𝐴) ∈ ℂ → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴)) |
127 | 124, 126 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴)) |
128 | 120, 127 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / 2) = (𝐶 − 𝐴)) |
129 | 128 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
(((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / 2) / 2) =
((𝐶 − 𝐴) / 2)) |
130 | 25, 129 | eqtr3d 2646 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2 ·
2)) = ((𝐶 − 𝐴) / 2)) |
131 | 20, 130 | syl5eq 2656 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵)))↑2) / (2↑2))
= ((𝐶 − 𝐴) / 2)) |
132 | 18, 131 | eqtrd 2644 |
. 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) →
((((√‘(𝐶 +
𝐵)) −
(√‘(𝐶 −
𝐵))) / 2)↑2) = ((𝐶 − 𝐴) / 2)) |
133 | 2, 132 | syl5eq 2656 |
1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2)) |