Step | Hyp | Ref
| Expression |
1 | | flt4lem5elem.2 |
. . . . 5
⊢ (𝜑 → (𝑅 gcd 𝑆) = 1) |
2 | | flt4lem5elem.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) |
3 | | flt4lem5elem.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ℕ) |
4 | 2, 3 | prmdvdsncoprmbd 16431 |
. . . . . 6
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆) ↔ (𝑅 gcd 𝑆) ≠ 1)) |
5 | 4 | necon2bbid 2987 |
. . . . 5
⊢ (𝜑 → ((𝑅 gcd 𝑆) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) |
6 | 1, 5 | mpbid 231 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) |
7 | | simprl 768 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑅) |
8 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℙ) |
9 | | prmz 16380 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℤ) |
11 | | flt4lem5elem.m |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
12 | 11 | nnzd 12425 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 12 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑀 ∈ ℤ) |
14 | 2 | nnsqcld 13959 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅↑2) ∈ ℕ) |
15 | 14 | nnzd 12425 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅↑2) ∈ ℤ) |
16 | 15 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℤ) |
17 | | simprr 770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑀) |
18 | 2 | nnzd 12425 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℤ) |
19 | 18 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑅 ∈ ℤ) |
20 | | prmdvdssq 16423 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℤ) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) |
21 | 8, 19, 20 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) |
22 | 7, 21 | mpbid 231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑅↑2)) |
23 | 10, 13, 16, 17, 22 | dvds2subd 16002 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑀 − (𝑅↑2))) |
24 | 14 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅↑2) ∈ ℂ) |
25 | 24 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℂ) |
26 | 3 | nnsqcld 13959 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆↑2) ∈ ℕ) |
27 | 26 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆↑2) ∈ ℂ) |
28 | 27 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℂ) |
29 | | flt4lem5elem.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2))) |
30 | 29 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑀 = ((𝑅↑2) + (𝑆↑2))) |
31 | 25, 28, 30 | mvrladdd 11388 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑀 − (𝑅↑2)) = (𝑆↑2)) |
32 | 23, 31 | breqtrd 5100 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑆↑2)) |
33 | 3 | nnzd 12425 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℤ) |
34 | 33 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑆 ∈ ℤ) |
35 | | prmdvdssq 16423 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ 𝑆 ∈ ℤ) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) |
36 | 8, 34, 35 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) |
37 | 32, 36 | mpbird 256 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑆) |
38 | 7, 37 | jca 512 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) |
39 | 38 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) |
40 | 39 | reximdva 3203 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) |
41 | 6, 40 | mtod 197 |
. . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀)) |
42 | 2, 11 | prmdvdsncoprmbd 16431 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀) ↔ (𝑅 gcd 𝑀) ≠ 1)) |
43 | 42 | necon2bbid 2987 |
. . 3
⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑀))) |
44 | 41, 43 | mpbird 256 |
. 2
⊢ (𝜑 → (𝑅 gcd 𝑀) = 1) |
45 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℙ) |
46 | 45, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∈ ℤ) |
47 | 12 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑀 ∈ ℤ) |
48 | 26 | nnzd 12425 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆↑2) ∈ ℤ) |
49 | 48 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℤ) |
50 | | simprr 770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑀) |
51 | | simprl 768 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑆) |
52 | 33 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑆 ∈ ℤ) |
53 | 45, 52, 35 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑆 ↔ 𝑝 ∥ (𝑆↑2))) |
54 | 51, 53 | mpbid 231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑆↑2)) |
55 | 46, 47, 49, 50, 54 | dvds2subd 16002 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑀 − (𝑆↑2))) |
56 | 24 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑅↑2) ∈ ℂ) |
57 | 27 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑆↑2) ∈ ℂ) |
58 | 29 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑀 = ((𝑅↑2) + (𝑆↑2))) |
59 | 56, 57, 58 | mvrraddd 11387 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑀 − (𝑆↑2)) = (𝑅↑2)) |
60 | 55, 59 | breqtrd 5100 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ (𝑅↑2)) |
61 | 18 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑅 ∈ ℤ) |
62 | 45, 61, 20 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ↔ 𝑝 ∥ (𝑅↑2))) |
63 | 60, 62 | mpbird 256 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → 𝑝 ∥ 𝑅) |
64 | 63, 51 | jca 512 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆)) |
65 | 64 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) → (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) |
66 | 65 | reximdva 3203 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ 𝑝 ∥ 𝑆))) |
67 | 6, 66 | mtod 197 |
. . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀)) |
68 | 3, 11 | prmdvdsncoprmbd 16431 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀) ↔ (𝑆 gcd 𝑀) ≠ 1)) |
69 | 68 | necon2bbid 2987 |
. . 3
⊢ (𝜑 → ((𝑆 gcd 𝑀) = 1 ↔ ¬ ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑆 ∧ 𝑝 ∥ 𝑀))) |
70 | 67, 69 | mpbird 256 |
. 2
⊢ (𝜑 → (𝑆 gcd 𝑀) = 1) |
71 | 44, 70 | jca 512 |
1
⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1)) |