| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | flt4lem5elem.2 | . . . . 5
⊢ (𝜑 → (𝑅 gcd 𝑆) = 1) | 
| 2 |  | flt4lem5elem.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 3 |  | flt4lem5elem.s | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ℕ) | 
| 4 | 2, 3 | prmdvdsncoprmbd 16765 | . . . . . 6
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆) ↔ (𝑅 gcd 𝑆) ≠ 1)) | 
| 5 | 4 | necon2bbid 2983 | . . . . 5
⊢ (𝜑 → ((𝑅 gcd 𝑆) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) | 
| 6 | 1, 5 | mpbid 232 | . . . 4
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) | 
| 7 |  | simprl 770 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑅) | 
| 8 |  | simplr 768 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℙ) | 
| 9 |  | prmz 16713 | . . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℤ) | 
| 11 |  | flt4lem5elem.m | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 12 | 11 | nnzd 12642 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 13 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑀 ∈ ℤ) | 
| 14 | 2 | nnsqcld 14284 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑅↑2) ∈ ℕ) | 
| 15 | 14 | nnzd 12642 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅↑2) ∈ ℤ) | 
| 16 | 15 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℤ) | 
| 17 |  | simprr 772 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑀) | 
| 18 | 2 | nnzd 12642 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℤ) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑅 ∈ ℤ) | 
| 20 |  | prmdvdssq 16756 | . . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℤ) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) | 
| 21 | 8, 19, 20 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) | 
| 22 | 7, 21 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑅↑2)) | 
| 23 | 10, 13, 16, 17, 22 | dvds2subd 16331 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑀 − (𝑅↑2))) | 
| 24 | 14 | nncnd 12283 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅↑2) ∈ ℂ) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℂ) | 
| 26 | 3 | nnsqcld 14284 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆↑2) ∈ ℕ) | 
| 27 | 26 | nncnd 12283 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆↑2) ∈ ℂ) | 
| 28 | 27 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℂ) | 
| 29 |  | flt4lem5elem.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2))) | 
| 30 | 29 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑀 = ((𝑅↑2) + (𝑆↑2))) | 
| 31 | 25, 28, 30 | mvrladdd 11677 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑀 − (𝑅↑2)) = (𝑆↑2)) | 
| 32 | 23, 31 | breqtrd 5168 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑆↑2)) | 
| 33 | 3 | nnzd 12642 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℤ) | 
| 34 | 33 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑆 ∈ ℤ) | 
| 35 |  | prmdvdssq 16756 | . . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ 𝑆 ∈ ℤ) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) | 
| 36 | 8, 34, 35 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) | 
| 37 | 32, 36 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑆) | 
| 38 | 7, 37 | jca 511 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) | 
| 39 | 38 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) | 
| 40 | 39 | reximdva 3167 | . . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) | 
| 41 | 6, 40 | mtod 198 | . . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) | 
| 42 | 2, 11 | prmdvdsncoprmbd 16765 | . . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) ↔ (𝑅 gcd 𝑀) ≠ 1)) | 
| 43 | 42 | necon2bbid 2983 | . . 3
⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀))) | 
| 44 | 41, 43 | mpbird 257 | . 2
⊢ (𝜑 → (𝑅 gcd 𝑀) = 1) | 
| 45 |  | simplr 768 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℙ) | 
| 46 | 45, 9 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℤ) | 
| 47 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑀 ∈ ℤ) | 
| 48 | 26 | nnzd 12642 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆↑2) ∈ ℤ) | 
| 49 | 48 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℤ) | 
| 50 |  | simprr 772 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑀) | 
| 51 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑆) | 
| 52 | 33 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑆 ∈ ℤ) | 
| 53 | 45, 52, 35 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) | 
| 54 | 51, 53 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑆↑2)) | 
| 55 | 46, 47, 49, 50, 54 | dvds2subd 16331 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑀 − (𝑆↑2))) | 
| 56 | 24 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℂ) | 
| 57 | 27 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℂ) | 
| 58 | 29 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑀 = ((𝑅↑2) + (𝑆↑2))) | 
| 59 | 56, 57, 58 | mvrraddd 11676 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑀 − (𝑆↑2)) = (𝑅↑2)) | 
| 60 | 55, 59 | breqtrd 5168 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑅↑2)) | 
| 61 | 18 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑅 ∈ ℤ) | 
| 62 | 45, 61, 20 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) | 
| 63 | 60, 62 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑅) | 
| 64 | 63, 51 | jca 511 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) | 
| 65 | 64 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) | 
| 66 | 65 | reximdva 3167 | . . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) | 
| 67 | 6, 66 | mtod 198 | . . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) | 
| 68 | 3, 11 | prmdvdsncoprmbd 16765 | . . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) ↔ (𝑆 gcd 𝑀) ≠ 1)) | 
| 69 | 68 | necon2bbid 2983 | . . 3
⊢ (𝜑 → ((𝑆 gcd 𝑀) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀))) | 
| 70 | 67, 69 | mpbird 257 | . 2
⊢ (𝜑 → (𝑆 gcd 𝑀) = 1) | 
| 71 | 44, 70 | jca 511 | 1
⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1)) |