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