| 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 16686 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) | 
| 5 | 2, 3, 4 | syl2anc 584 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) | 
| 6 | 1, 5 | mpbird 257 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1)) | 
| 7 |  | simplr 769 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∈ ℕ) | 
| 8 | 7 | nnzd 12640 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∈ ℤ) | 
| 9 |  | flt4lem5.1 | . . . . . . . . . . . . 13
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) | 
| 10 | 9 | pythagtriplem11 16863 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑀 ∈ ℕ) | 
| 11 | 10 | ad2antrr 726 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑀 ∈ ℕ) | 
| 12 | 11 | nnsqcld 14283 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀↑2) ∈ ℕ) | 
| 13 | 12 | nnzd 12640 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀↑2) ∈ ℤ) | 
| 14 |  | flt4lem5.2 | . . . . . . . . . . . . 13
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) | 
| 15 | 14 | pythagtriplem13 16865 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑁 ∈ ℕ) | 
| 16 | 15 | ad2antrr 726 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑁 ∈ ℕ) | 
| 17 | 16 | nnsqcld 14283 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑁↑2) ∈ ℕ) | 
| 18 | 17 | nnzd 12640 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑁↑2) ∈ ℤ) | 
| 19 |  | simprl 771 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝑀) | 
| 20 | 11 | nnzd 12640 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑀 ∈ ℤ) | 
| 21 |  | 2nn 12339 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ | 
| 22 | 21 | a1i 11 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 2 ∈ ℕ) | 
| 23 |  | dvdsexp2im 16364 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑖 ∥
𝑀 → 𝑖 ∥ (𝑀↑2))) | 
| 24 | 8, 20, 22, 23 | syl3anc 1373 | . . . . . . . . . 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 12640 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑁 ∈ ℤ) | 
| 28 |  | dvdsexp2im 16364 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑖 ∥
𝑁 → 𝑖 ∥ (𝑁↑2))) | 
| 29 | 8, 27, 22, 28 | syl3anc 1373 | . . . . . . . . . 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 16330 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ ((𝑀↑2) − (𝑁↑2))) | 
| 32 | 9, 14 | pythagtriplem15 16867 | . . . . . . . . 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 5171 | . . . . . . 7
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝐴) | 
| 35 |  | 2z 12649 | . . . . . . . . . 10
⊢ 2 ∈
ℤ | 
| 36 | 35 | a1i 11 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 2 ∈ ℤ) | 
| 37 | 11, 16 | nnmulcld 12319 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀 · 𝑁) ∈ ℕ) | 
| 38 | 37 | nnzd 12640 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑀 · 𝑁) ∈ ℤ) | 
| 39 | 8, 20, 27, 26 | dvdsmultr2d 16336 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (𝑀 · 𝑁)) | 
| 40 | 8, 36, 38, 39 | dvdsmultr2d 16336 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ (2 · (𝑀 · 𝑁))) | 
| 41 | 9, 14 | pythagtriplem16 16868 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 = (2 · (𝑀 · 𝑁))) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝐵 = (2 · (𝑀 · 𝑁))) | 
| 43 | 40, 42 | breqtrrd 5171 | . . . . . . 7
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → 𝑖 ∥ 𝐵) | 
| 44 | 34, 43 | jca 511 | . . . . . 6
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐶 ∈
ℕ) ∧ ((𝐴↑2)
+ (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁)) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) | 
| 45 | 44 | ex 412 | . . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) → ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) | 
| 46 | 45 | imim1d 82 | . . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) ∧ 𝑖 ∈ ℕ) → (((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1))) | 
| 47 | 46 | ralimdva 3167 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1))) | 
| 48 | 6, 47 | mpd 15 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1)) | 
| 49 |  | coprmgcdb 16686 | . . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1) ↔ (𝑀 gcd 𝑁) = 1)) | 
| 50 | 10, 15, 49 | syl2anc 584 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝑀 ∧ 𝑖 ∥ 𝑁) → 𝑖 = 1) ↔ (𝑀 gcd 𝑁) = 1)) | 
| 51 | 48, 50 | mpbid 232 | 1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1) |