Step |
Hyp |
Ref |
Expression |
1 |
|
ppiublem1.1 |
⊢ ( 𝑁 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑁 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
2 |
|
ppiublem1.2 |
⊢ 𝑀 ∈ ℕ0 |
3 |
|
ppiublem1.3 |
⊢ 𝑁 = ( 𝑀 + 1 ) |
4 |
|
ppiublem1.4 |
⊢ ( 2 ∥ 𝑀 ∨ 3 ∥ 𝑀 ∨ 𝑀 ∈ { 1 , 5 } ) |
5 |
1
|
simpli |
⊢ 𝑁 ≤ 6 |
6 |
|
df-6 |
⊢ 6 = ( 5 + 1 ) |
7 |
5 3 6
|
3brtr3i |
⊢ ( 𝑀 + 1 ) ≤ ( 5 + 1 ) |
8 |
2
|
nn0rei |
⊢ 𝑀 ∈ ℝ |
9 |
|
5re |
⊢ 5 ∈ ℝ |
10 |
|
1re |
⊢ 1 ∈ ℝ |
11 |
8 9 10
|
leadd1i |
⊢ ( 𝑀 ≤ 5 ↔ ( 𝑀 + 1 ) ≤ ( 5 + 1 ) ) |
12 |
7 11
|
mpbir |
⊢ 𝑀 ≤ 5 |
13 |
|
6re |
⊢ 6 ∈ ℝ |
14 |
|
5lt6 |
⊢ 5 < 6 |
15 |
9 13 14
|
ltleii |
⊢ 5 ≤ 6 |
16 |
8 9 13
|
letri |
⊢ ( ( 𝑀 ≤ 5 ∧ 5 ≤ 6 ) → 𝑀 ≤ 6 ) |
17 |
12 15 16
|
mp2an |
⊢ 𝑀 ≤ 6 |
18 |
2
|
nn0zi |
⊢ 𝑀 ∈ ℤ |
19 |
|
5nn |
⊢ 5 ∈ ℕ |
20 |
19
|
nnzi |
⊢ 5 ∈ ℤ |
21 |
|
eluz2 |
⊢ ( 5 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 5 ∈ ℤ ∧ 𝑀 ≤ 5 ) ) |
22 |
18 20 12 21
|
mpbir3an |
⊢ 5 ∈ ( ℤ≥ ‘ 𝑀 ) |
23 |
|
elfzp12 |
⊢ ( 5 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) ↔ ( ( 𝑃 mod 6 ) = 𝑀 ∨ ( 𝑃 mod 6 ) ∈ ( ( 𝑀 + 1 ) ... 5 ) ) ) ) |
24 |
22 23
|
ax-mp |
⊢ ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) ↔ ( ( 𝑃 mod 6 ) = 𝑀 ∨ ( 𝑃 mod 6 ) ∈ ( ( 𝑀 + 1 ) ... 5 ) ) ) |
25 |
|
2nn |
⊢ 2 ∈ ℕ |
26 |
|
6nn |
⊢ 6 ∈ ℕ |
27 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
28 |
27
|
adantr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → 𝑃 ∈ ℤ ) |
29 |
|
3z |
⊢ 3 ∈ ℤ |
30 |
|
2z |
⊢ 2 ∈ ℤ |
31 |
|
dvdsmul2 |
⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( 3 · 2 ) ) |
32 |
29 30 31
|
mp2an |
⊢ 2 ∥ ( 3 · 2 ) |
33 |
|
3t2e6 |
⊢ ( 3 · 2 ) = 6 |
34 |
32 33
|
breqtri |
⊢ 2 ∥ 6 |
35 |
|
dvdsmod |
⊢ ( ( ( 2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ ) ∧ 2 ∥ 6 ) → ( 2 ∥ ( 𝑃 mod 6 ) ↔ 2 ∥ 𝑃 ) ) |
36 |
34 35
|
mpan2 |
⊢ ( ( 2 ∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ ) → ( 2 ∥ ( 𝑃 mod 6 ) ↔ 2 ∥ 𝑃 ) ) |
37 |
25 26 28 36
|
mp3an12i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 ∥ ( 𝑃 mod 6 ) ↔ 2 ∥ 𝑃 ) ) |
38 |
|
uzid |
⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) ) |
39 |
30 38
|
ax-mp |
⊢ 2 ∈ ( ℤ≥ ‘ 2 ) |
40 |
|
simpl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → 𝑃 ∈ ℙ ) |
41 |
|
dvdsprm |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) ) |
42 |
39 40 41
|
sylancr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) ) |
43 |
37 42
|
bitrd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 ∥ ( 𝑃 mod 6 ) ↔ 2 = 𝑃 ) ) |
44 |
|
simpr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → 4 ≤ 𝑃 ) |
45 |
|
breq2 |
⊢ ( 2 = 𝑃 → ( 4 ≤ 2 ↔ 4 ≤ 𝑃 ) ) |
46 |
44 45
|
syl5ibrcom |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 = 𝑃 → 4 ≤ 2 ) ) |
47 |
|
2lt4 |
⊢ 2 < 4 |
48 |
|
2re |
⊢ 2 ∈ ℝ |
49 |
|
4re |
⊢ 4 ∈ ℝ |
50 |
48 49
|
ltnlei |
⊢ ( 2 < 4 ↔ ¬ 4 ≤ 2 ) |
51 |
47 50
|
mpbi |
⊢ ¬ 4 ≤ 2 |
52 |
51
|
pm2.21i |
⊢ ( 4 ≤ 2 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) |
53 |
46 52
|
syl6 |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 = 𝑃 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
54 |
43 53
|
sylbid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 2 ∥ ( 𝑃 mod 6 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
55 |
|
breq2 |
⊢ ( ( 𝑃 mod 6 ) = 𝑀 → ( 2 ∥ ( 𝑃 mod 6 ) ↔ 2 ∥ 𝑀 ) ) |
56 |
55
|
imbi1d |
⊢ ( ( 𝑃 mod 6 ) = 𝑀 → ( ( 2 ∥ ( 𝑃 mod 6 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ↔ ( 2 ∥ 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
57 |
54 56
|
syl5ibcom |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 2 ∥ 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
58 |
57
|
com3r |
⊢ ( 2 ∥ 𝑀 → ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
59 |
|
3nn |
⊢ 3 ∈ ℕ |
60 |
|
dvdsmul1 |
⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → 3 ∥ ( 3 · 2 ) ) |
61 |
29 30 60
|
mp2an |
⊢ 3 ∥ ( 3 · 2 ) |
62 |
61 33
|
breqtri |
⊢ 3 ∥ 6 |
63 |
|
dvdsmod |
⊢ ( ( ( 3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ ) ∧ 3 ∥ 6 ) → ( 3 ∥ ( 𝑃 mod 6 ) ↔ 3 ∥ 𝑃 ) ) |
64 |
62 63
|
mpan2 |
⊢ ( ( 3 ∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ ) → ( 3 ∥ ( 𝑃 mod 6 ) ↔ 3 ∥ 𝑃 ) ) |
65 |
59 26 28 64
|
mp3an12i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 ∥ ( 𝑃 mod 6 ) ↔ 3 ∥ 𝑃 ) ) |
66 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
67 |
|
peano2uz |
⊢ ( 2 ∈ ( ℤ≥ ‘ 2 ) → ( 2 + 1 ) ∈ ( ℤ≥ ‘ 2 ) ) |
68 |
39 67
|
ax-mp |
⊢ ( 2 + 1 ) ∈ ( ℤ≥ ‘ 2 ) |
69 |
66 68
|
eqeltri |
⊢ 3 ∈ ( ℤ≥ ‘ 2 ) |
70 |
|
dvdsprm |
⊢ ( ( 3 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 3 ∥ 𝑃 ↔ 3 = 𝑃 ) ) |
71 |
69 40 70
|
sylancr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 ∥ 𝑃 ↔ 3 = 𝑃 ) ) |
72 |
65 71
|
bitrd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 ∥ ( 𝑃 mod 6 ) ↔ 3 = 𝑃 ) ) |
73 |
|
breq2 |
⊢ ( 3 = 𝑃 → ( 4 ≤ 3 ↔ 4 ≤ 𝑃 ) ) |
74 |
44 73
|
syl5ibrcom |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 = 𝑃 → 4 ≤ 3 ) ) |
75 |
|
3lt4 |
⊢ 3 < 4 |
76 |
|
3re |
⊢ 3 ∈ ℝ |
77 |
76 49
|
ltnlei |
⊢ ( 3 < 4 ↔ ¬ 4 ≤ 3 ) |
78 |
75 77
|
mpbi |
⊢ ¬ 4 ≤ 3 |
79 |
78
|
pm2.21i |
⊢ ( 4 ≤ 3 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) |
80 |
74 79
|
syl6 |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 = 𝑃 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
81 |
72 80
|
sylbid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 3 ∥ ( 𝑃 mod 6 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
82 |
|
breq2 |
⊢ ( ( 𝑃 mod 6 ) = 𝑀 → ( 3 ∥ ( 𝑃 mod 6 ) ↔ 3 ∥ 𝑀 ) ) |
83 |
82
|
imbi1d |
⊢ ( ( 𝑃 mod 6 ) = 𝑀 → ( ( 3 ∥ ( 𝑃 mod 6 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ↔ ( 3 ∥ 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
84 |
81 83
|
syl5ibcom |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 3 ∥ 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
85 |
84
|
com3r |
⊢ ( 3 ∥ 𝑀 → ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
86 |
|
eleq1a |
⊢ ( 𝑀 ∈ { 1 , 5 } → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
87 |
86
|
a1d |
⊢ ( 𝑀 ∈ { 1 , 5 } → ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
88 |
58 85 87
|
3jaoi |
⊢ ( ( 2 ∥ 𝑀 ∨ 3 ∥ 𝑀 ∨ 𝑀 ∈ { 1 , 5 } ) → ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
89 |
4 88
|
ax-mp |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) = 𝑀 → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
90 |
3
|
oveq1i |
⊢ ( 𝑁 ... 5 ) = ( ( 𝑀 + 1 ) ... 5 ) |
91 |
90
|
eleq2i |
⊢ ( ( 𝑃 mod 6 ) ∈ ( 𝑁 ... 5 ) ↔ ( 𝑃 mod 6 ) ∈ ( ( 𝑀 + 1 ) ... 5 ) ) |
92 |
1
|
simpri |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑁 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
93 |
91 92
|
syl5bir |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( ( 𝑀 + 1 ) ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
94 |
89 93
|
jaod |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( ( 𝑃 mod 6 ) = 𝑀 ∨ ( 𝑃 mod 6 ) ∈ ( ( 𝑀 + 1 ) ... 5 ) ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
95 |
24 94
|
syl5bi |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
96 |
17 95
|
pm3.2i |
⊢ ( 𝑀 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 𝑀 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |