Metamath Proof Explorer

Theorem ppiublem2

Description: A prime greater than 3 does not divide 2 or 3 , so its residue mod 6 is 1 or 5 . (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Assertion ppiublem2 ⊢P∈ℙ∧4≤P→Pmod6∈15

Proof

Step Hyp Ref Expression
1 prmz ⊢P∈ℙ→P∈ℤ
2 1 adantr ⊢P∈ℙ∧4≤P→P∈ℤ
3 6nn ⊢6∈ℕ
4 zmodfz ⊢P∈ℤ∧6∈ℕ→Pmod6∈0…6−1
5 2 3 4 sylancl ⊢P∈ℙ∧4≤P→Pmod6∈0…6−1
6 6m1e5 ⊢6−1=5
7 6 oveq2i ⊢0…6−1=0…5
8 5 7 eleqtrdi ⊢P∈ℙ∧4≤P→Pmod6∈0…5
9 6re ⊢6∈ℝ
10 9 leidi ⊢6≤6
11 noel ⊢¬Pmod6∈∅
12 11 pm2.21i ⊢Pmod6∈∅→Pmod6∈15
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 ⊢Pmod6∈6…5→Pmod6∈15
21 20 a1i ⊢P∈ℙ∧4≤P→Pmod6∈6…5→Pmod6∈15
22 10 21 pm3.2i ⊢6≤6∧P∈ℙ∧4≤P→Pmod6∈6…5→Pmod6∈15
23 5nn0 ⊢5∈ℕ0
24 df-6 ⊢6=5+1
25 15 elexi ⊢5∈V
26 25 prid2 ⊢5∈15
27 26 3mix3i ⊢2∥5∨3∥5∨5∈15
28 22 23 24 27 ppiublem1 ⊢5≤6∧P∈ℙ∧4≤P→Pmod6∈5…5→Pmod6∈15
29 4nn0 ⊢4∈ℕ0
30 df-5 ⊢5=4+1
31 z4even ⊢2∥4
32 31 3mix1i ⊢2∥4∨3∥4∨4∈15
33 28 29 30 32 ppiublem1 ⊢4≤6∧P∈ℙ∧4≤P→Pmod6∈4…5→Pmod6∈15
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∈15
40 33 34 35 39 ppiublem1 ⊢3≤6∧P∈ℙ∧4≤P→Pmod6∈3…5→Pmod6∈15
41 2nn0 ⊢2∈ℕ0
42 df-3 ⊢3=2+1
43 z2even ⊢2∥2
44 43 3mix1i ⊢2∥2∨3∥2∨2∈15
45 40 41 42 44 ppiublem1 ⊢2≤6∧P∈ℙ∧4≤P→Pmod6∈2…5→Pmod6∈15
46 1nn0 ⊢1∈ℕ0
47 df-2 ⊢2=1+1
48 1ex ⊢1∈V
49 48 prid1 ⊢1∈15
50 49 3mix3i ⊢2∥1∨3∥1∨1∈15
51 45 46 47 50 ppiublem1 ⊢1≤6∧P∈ℙ∧4≤P→Pmod6∈1…5→Pmod6∈15
52 0nn0 ⊢0∈ℕ0
53 1e0p1 ⊢1=0+1
54 z0even ⊢2∥0
55 54 3mix1i ⊢2∥0∨3∥0∨0∈15
56 51 52 53 55 ppiublem1 ⊢0≤6∧P∈ℙ∧4≤P→Pmod6∈0…5→Pmod6∈15
57 56 simpri ⊢P∈ℙ∧4≤P→Pmod6∈0…5→Pmod6∈15
58 8 57 mpd ⊢P∈ℙ∧4≤P→Pmod6∈15