Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐴 gcd 𝐵) = 1) |
2 | | simp11 1204 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℕ) |
3 | | simp12 1205 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℕ) |
4 | | coprmgcdb 16083 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) |
5 | 2, 3, 4 | syl2anc 587 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) |
6 | 1, 5 | mpbird 260 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1)) |
7 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∈ ℕ) |
8 | 7 | nnzd 12160 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∈ ℤ) |
9 | | flt4lem5.1 |
. . . . . . . . . . . . 13
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) |
10 | 9 | pythagtriplem11 16255 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑀 ∈ ℕ) |
11 | 10 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑀 ∈ ℕ) |
12 | 11 | nnsqcld 13690 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀↑2) ∈ ℕ) |
13 | 12 | nnzd 12160 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀↑2) ∈ ℤ) |
14 | | flt4lem5.2 |
. . . . . . . . . . . . 13
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) |
15 | 14 | pythagtriplem13 16257 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑁 ∈ ℕ) |
16 | 15 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑁 ∈ ℕ) |
17 | 16 | nnsqcld 13690 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑁↑2) ∈ ℕ) |
18 | 17 | nnzd 12160 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑁↑2) ∈ ℤ) |
19 | | simprl 771 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝑀) |
20 | 11 | nnzd 12160 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑀 ∈ ℤ) |
21 | | 2nn 11782 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 2 ∈ ℕ) |
23 | | dvdsexp2im 15765 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑖 ∥
𝑀 → 𝑖 ∥ (𝑀↑2))) |
24 | 8, 20, 22, 23 | syl3anc 1372 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑖 ∥ 𝑀 → 𝑖 ∥ (𝑀↑2))) |
25 | 19, 24 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (𝑀↑2)) |
26 | | simprr 773 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝑁) |
27 | 16 | nnzd 12160 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑁 ∈ ℤ) |
28 | | dvdsexp2im 15765 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑖 ∥
𝑁 → 𝑖 ∥ (𝑁↑2))) |
29 | 8, 27, 22, 28 | syl3anc 1372 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑖 ∥ 𝑁 → 𝑖 ∥ (𝑁↑2))) |
30 | 26, 29 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (𝑁↑2)) |
31 | 8, 13, 18, 25, 30 | dvds2subd 15731 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ ((𝑀↑2) − (𝑁↑2))) |
32 | 9, 14 | pythagtriplem15 16259 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 = ((𝑀↑2) − (𝑁↑2))) |
33 | 32 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝐴 = ((𝑀↑2) − (𝑁↑2))) |
34 | 31, 33 | breqtrrd 5055 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝐴) |
35 | | 2z 12088 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 2 ∈ ℤ) |
37 | 11, 16 | nnmulcld 11762 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀 · 𝑁) ∈ ℕ) |
38 | 37 | nnzd 12160 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀 · 𝑁) ∈ ℤ) |
39 | 8, 20, 27, 26 | dvdsmultr2d 15737 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (𝑀 · 𝑁)) |
40 | 8, 36, 38, 39 | dvdsmultr2d 15737 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (2 · (𝑀 · 𝑁))) |
41 | 9, 14 | pythagtriplem16 16260 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 = (2 · (𝑀 · 𝑁))) |
42 | 41 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝐵 = (2 · (𝑀 · 𝑁))) |
43 | 40, 42 | breqtrrd 5055 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝐵) |
44 | 34, 43 | jca 515 |
. . . . . 6
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
45 | 44 | ex 416 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) → ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
46 | 45 | imim1d 82 |
. . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) → (((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1))) |
47 | 46 | ralimdva 3091 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1))) |
48 | 6, 47 | mpd 15 |
. 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1)) |
49 | | coprmgcdb 16083 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1) ↔ (𝑀 gcd 𝑁) = 1)) |
50 | 10, 15, 49 | syl2anc 587 |
. 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1) ↔ (𝑀 gcd 𝑁) = 1)) |
51 | 48, 50 | mpbid 235 |
1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1) |