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 ( ( 𝑃 ∈ ℙ ∧ 4 ≤ 𝑃 ) → ( 𝑃 mod 6 ) ∈ { 1 , 5 } )

Proof

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 } )