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 e. Prime /\ 4 <_ P ) -> ( P mod 6 ) e. { 1 , 5 } )

Proof

Step Hyp Ref Expression
1 prmz 
 |-  ( P e. Prime -> P e. ZZ )
2 1 adantr 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> P e. ZZ )
3 6nn 
 |-  6 e. NN
4 zmodfz 
 |-  ( ( P e. ZZ /\ 6 e. NN ) -> ( P mod 6 ) e. ( 0 ... ( 6 - 1 ) ) )
5 2 3 4 sylancl 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( P mod 6 ) e. ( 0 ... ( 6 - 1 ) ) )
6 6m1e5 
 |-  ( 6 - 1 ) = 5
7 6 oveq2i 
 |-  ( 0 ... ( 6 - 1 ) ) = ( 0 ... 5 )
8 5 7 eleqtrdi 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( P mod 6 ) e. ( 0 ... 5 ) )
9 6re 
 |-  6 e. RR
10 9 leidi 
 |-  6 <_ 6
11 noel 
 |-  -. ( P mod 6 ) e. (/)
12 11 pm2.21i 
 |-  ( ( P mod 6 ) e. (/) -> ( P mod 6 ) e. { 1 , 5 } )
13 5lt6 
 |-  5 < 6
14 3 nnzi 
 |-  6 e. ZZ
15 5nn 
 |-  5 e. NN
16 15 nnzi 
 |-  5 e. ZZ
17 fzn 
 |-  ( ( 6 e. ZZ /\ 5 e. ZZ ) -> ( 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 ) e. ( 6 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } )
21 20 a1i 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 6 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
22 10 21 pm3.2i 
 |-  ( 6 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 6 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
23 5nn0 
 |-  5 e. NN0
24 df-6 
 |-  6 = ( 5 + 1 )
25 15 elexi 
 |-  5 e. _V
26 25 prid2 
 |-  5 e. { 1 , 5 }
27 26 3mix3i 
 |-  ( 2 || 5 \/ 3 || 5 \/ 5 e. { 1 , 5 } )
28 22 23 24 27 ppiublem1 
 |-  ( 5 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 5 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
29 4nn0 
 |-  4 e. NN0
30 df-5 
 |-  5 = ( 4 + 1 )
31 z4even 
 |-  2 || 4
32 31 3mix1i 
 |-  ( 2 || 4 \/ 3 || 4 \/ 4 e. { 1 , 5 } )
33 28 29 30 32 ppiublem1 
 |-  ( 4 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 4 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
34 3nn0 
 |-  3 e. NN0
35 df-4 
 |-  4 = ( 3 + 1 )
36 3z 
 |-  3 e. ZZ
37 iddvds 
 |-  ( 3 e. ZZ -> 3 || 3 )
38 36 37 ax-mp 
 |-  3 || 3
39 38 3mix2i 
 |-  ( 2 || 3 \/ 3 || 3 \/ 3 e. { 1 , 5 } )
40 33 34 35 39 ppiublem1 
 |-  ( 3 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 3 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
41 2nn0 
 |-  2 e. NN0
42 df-3 
 |-  3 = ( 2 + 1 )
43 z2even 
 |-  2 || 2
44 43 3mix1i 
 |-  ( 2 || 2 \/ 3 || 2 \/ 2 e. { 1 , 5 } )
45 40 41 42 44 ppiublem1 
 |-  ( 2 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 2 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
46 1nn0 
 |-  1 e. NN0
47 df-2 
 |-  2 = ( 1 + 1 )
48 1ex 
 |-  1 e. _V
49 48 prid1 
 |-  1 e. { 1 , 5 }
50 49 3mix3i 
 |-  ( 2 || 1 \/ 3 || 1 \/ 1 e. { 1 , 5 } )
51 45 46 47 50 ppiublem1 
 |-  ( 1 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 1 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
52 0nn0 
 |-  0 e. NN0
53 1e0p1 
 |-  1 = ( 0 + 1 )
54 z0even 
 |-  2 || 0
55 54 3mix1i 
 |-  ( 2 || 0 \/ 3 || 0 \/ 0 e. { 1 , 5 } )
56 51 52 53 55 ppiublem1 
 |-  ( 0 <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 0 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
57 56 simpri 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( 0 ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
58 8 57 mpd 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( P mod 6 ) e. { 1 , 5 } )