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 → P mod 6 ∈ 1 5

Proof

Step Hyp Ref Expression
1 prmz ⊢ P ∈ ℙ → P ∈ ℤ
2 1 adantr ⊢ P ∈ ℙ ∧ 4 ≤ P → P ∈ ℤ
3 6nn ⊢ 6 ∈ ℕ
4 zmodfz ⊢ P ∈ ℤ ∧ 6 ∈ ℕ → P mod 6 ∈ 0 … 6 − 1
5 2 3 4 sylancl ⊢ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 0 … 6 − 1
6 6m1e5 ⊢ 6 − 1 = 5
7 6 oveq2i ⊢ 0 … 6 − 1 = 0 … 5
8 5 7 eleqtrdi ⊢ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 0 … 5
9 6re ⊢ 6 ∈ ℝ
10 9 leidi ⊢ 6 ≤ 6
11 noel ⊢ ¬ P mod 6 ∈ ∅
12 11 pm2.21i ⊢ P mod 6 ∈ ∅ → P 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 ⊢ P mod 6 ∈ 6 … 5 → P mod 6 ∈ 1 5
21 20 a1i ⊢ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 6 … 5 → P mod 6 ∈ 1 5
22 10 21 pm3.2i ⊢ 6 ≤ 6 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 6 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 5 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 4 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 3 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 2 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 1 … 5 → P 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 ∧ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 0 … 5 → P mod 6 ∈ 1 5
57 56 simpri ⊢ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 0 … 5 → P mod 6 ∈ 1 5
58 8 57 mpd ⊢ P ∈ ℙ ∧ 4 ≤ P → P mod 6 ∈ 1 5