Step |
Hyp |
Ref |
Expression |
1 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
2 |
1
|
adantr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → 𝑃 ∈ ℤ ) |
3 |
|
6nn |
⊢ 6 ∈ ℕ |
4 |
|
zmodfz |
⊢ ( ( 𝑃 ∈ ℤ ∧ 6 ∈ ℕ ) → ( 𝑃 mod 6 ) ∈ ( 0 ... ( 6 − 1 ) ) ) |
5 |
2 3 4
|
sylancl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 𝑃 mod 6 ) ∈ ( 0 ... ( 6 − 1 ) ) ) |
6 |
|
6m1e5 |
⊢ ( 6 − 1 ) = 5 |
7 |
6
|
oveq2i |
⊢ ( 0 ... ( 6 − 1 ) ) = ( 0 ... 5 ) |
8 |
5 7
|
eleqtrdi |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 𝑃 mod 6 ) ∈ ( 0 ... 5 ) ) |
9 |
|
6re |
⊢ 6 ∈ ℝ |
10 |
9
|
leidi |
⊢ 6 ≤ 6 |
11 |
|
noel |
⊢ ¬ ( 𝑃 mod 6 ) ∈ ∅ |
12 |
11
|
pm2.21i |
⊢ ( ( 𝑃 mod 6 ) ∈ ∅ → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) |
13 |
|
5lt6 |
⊢ 5 < 6 |
14 |
3
|
nnzi |
⊢ 6 ∈ ℤ |
15 |
|
5nn |
⊢ 5 ∈ ℕ |
16 |
15
|
nnzi |
⊢ 5 ∈ ℤ |
17 |
|
fzn |
⊢ ( ( 6 ∈ ℤ ∧ 5 ∈ ℤ ) → ( 5 < 6 ↔ ( 6 ... 5 ) = ∅ ) ) |
18 |
14 16 17
|
mp2an |
⊢ ( 5 < 6 ↔ ( 6 ... 5 ) = ∅ ) |
19 |
13 18
|
mpbi |
⊢ ( 6 ... 5 ) = ∅ |
20 |
12 19
|
eleq2s |
⊢ ( ( 𝑃 mod 6 ) ∈ ( 6 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) |
21 |
20
|
a1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 6 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
22 |
10 21
|
pm3.2i |
⊢ ( 6 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 6 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
23 |
|
5nn0 |
⊢ 5 ∈ ℕ0 |
24 |
|
df-6 |
⊢ 6 = ( 5 + 1 ) |
25 |
15
|
elexi |
⊢ 5 ∈ V |
26 |
25
|
prid2 |
⊢ 5 ∈ { 1 , 5 } |
27 |
26
|
3mix3i |
⊢ ( 2 ∥ 5 ∨ 3 ∥ 5 ∨ 5 ∈ { 1 , 5 } ) |
28 |
22 23 24 27
|
ppiublem1 |
⊢ ( 5 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 5 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
29 |
|
4nn0 |
⊢ 4 ∈ ℕ0 |
30 |
|
df-5 |
⊢ 5 = ( 4 + 1 ) |
31 |
|
z4even |
⊢ 2 ∥ 4 |
32 |
31
|
3mix1i |
⊢ ( 2 ∥ 4 ∨ 3 ∥ 4 ∨ 4 ∈ { 1 , 5 } ) |
33 |
28 29 30 32
|
ppiublem1 |
⊢ ( 4 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 4 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
34 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
35 |
|
df-4 |
⊢ 4 = ( 3 + 1 ) |
36 |
|
3z |
⊢ 3 ∈ ℤ |
37 |
|
iddvds |
⊢ ( 3 ∈ ℤ → 3 ∥ 3 ) |
38 |
36 37
|
ax-mp |
⊢ 3 ∥ 3 |
39 |
38
|
3mix2i |
⊢ ( 2 ∥ 3 ∨ 3 ∥ 3 ∨ 3 ∈ { 1 , 5 } ) |
40 |
33 34 35 39
|
ppiublem1 |
⊢ ( 3 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 3 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
41 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
42 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
43 |
|
z2even |
⊢ 2 ∥ 2 |
44 |
43
|
3mix1i |
⊢ ( 2 ∥ 2 ∨ 3 ∥ 2 ∨ 2 ∈ { 1 , 5 } ) |
45 |
40 41 42 44
|
ppiublem1 |
⊢ ( 2 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 2 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
46 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
47 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
48 |
|
1ex |
⊢ 1 ∈ V |
49 |
48
|
prid1 |
⊢ 1 ∈ { 1 , 5 } |
50 |
49
|
3mix3i |
⊢ ( 2 ∥ 1 ∨ 3 ∥ 1 ∨ 1 ∈ { 1 , 5 } ) |
51 |
45 46 47 50
|
ppiublem1 |
⊢ ( 1 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 1 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
52 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
53 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
54 |
|
z0even |
⊢ 2 ∥ 0 |
55 |
54
|
3mix1i |
⊢ ( 2 ∥ 0 ∨ 3 ∥ 0 ∨ 0 ∈ { 1 , 5 } ) |
56 |
51 52 53 55
|
ppiublem1 |
⊢ ( 0 ≤ 6 ∧ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 0 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) ) |
57 |
56
|
simpri |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( ( 𝑃 mod 6 ) ∈ ( 0 ... 5 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) ) |
58 |
8 57
|
mpd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } ) |