Metamath Proof Explorer

Theorem ppiublem1

Description: Lemma for ppiub . (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses ppiublem1.1 
|- ( N <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( N ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
ppiublem1.2 
|- M e. NN0
ppiublem1.3 
|- N = ( M + 1 )
ppiublem1.4 
|- ( 2 || M \/ 3 || M \/ M e. { 1 , 5 } )
Assertion ppiublem1 
|- ( M <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( M ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )

Proof

Step Hyp Ref Expression
1 ppiublem1.1 
 |-  ( N <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( N ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
2 ppiublem1.2 
 |-  M e. NN0
3 ppiublem1.3 
 |-  N = ( M + 1 )
4 ppiublem1.4 
 |-  ( 2 || M \/ 3 || M \/ M e. { 1 , 5 } )
5 1 simpli 
 |-  N <_ 6
6 df-6 
 |-  6 = ( 5 + 1 )
7 5 3 6 3brtr3i 
 |-  ( M + 1 ) <_ ( 5 + 1 )
8 2 nn0rei 
 |-  M e. RR
9 5re 
 |-  5 e. RR
10 1re 
 |-  1 e. RR
11 8 9 10 leadd1i 
 |-  ( M <_ 5 <-> ( M + 1 ) <_ ( 5 + 1 ) )
12 7 11 mpbir 
 |-  M <_ 5
13 6re 
 |-  6 e. RR
14 5lt6 
 |-  5 < 6
15 9 13 14 ltleii 
 |-  5 <_ 6
16 8 9 13 letri 
 |-  ( ( M <_ 5 /\ 5 <_ 6 ) -> M <_ 6 )
17 12 15 16 mp2an 
 |-  M <_ 6
18 2 nn0zi 
 |-  M e. ZZ
19 5nn 
 |-  5 e. NN
20 19 nnzi 
 |-  5 e. ZZ
21 eluz2 
 |-  ( 5 e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ 5 e. ZZ /\ M <_ 5 ) )
22 18 20 12 21 mpbir3an 
 |-  5 e. ( ZZ>= ` M )
23 elfzp12 
 |-  ( 5 e. ( ZZ>= ` M ) -> ( ( P mod 6 ) e. ( M ... 5 ) <-> ( ( P mod 6 ) = M \/ ( P mod 6 ) e. ( ( M + 1 ) ... 5 ) ) ) )
24 22 23 ax-mp 
 |-  ( ( P mod 6 ) e. ( M ... 5 ) <-> ( ( P mod 6 ) = M \/ ( P mod 6 ) e. ( ( M + 1 ) ... 5 ) ) )
25 2nn 
 |-  2 e. NN
26 6nn 
 |-  6 e. NN
27 prmz 
 |-  ( P e. Prime -> P e. ZZ )
28 27 adantr 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> P e. ZZ )
29 3z 
 |-  3 e. ZZ
30 2z 
 |-  2 e. ZZ
31 dvdsmul2 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> 2 || ( 3 x. 2 ) )
32 29 30 31 mp2an 
 |-  2 || ( 3 x. 2 )
33 3t2e6 
 |-  ( 3 x. 2 ) = 6
34 32 33 breqtri 
 |-  2 || 6
35 dvdsmod 
 |-  ( ( ( 2 e. NN /\ 6 e. NN /\ P e. ZZ ) /\ 2 || 6 ) -> ( 2 || ( P mod 6 ) <-> 2 || P ) )
36 34 35 mpan2 
 |-  ( ( 2 e. NN /\ 6 e. NN /\ P e. ZZ ) -> ( 2 || ( P mod 6 ) <-> 2 || P ) )
37 25 26 28 36 mp3an12i 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 || ( P mod 6 ) <-> 2 || P ) )
38 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
39 30 38 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
40 simpl 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> P e. Prime )
41 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) )
42 39 40 41 sylancr 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 || P <-> 2 = P ) )
43 37 42 bitrd 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 || ( P mod 6 ) <-> 2 = P ) )
44 simpr 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> 4 <_ P )
45 breq2 
 |-  ( 2 = P -> ( 4 <_ 2 <-> 4 <_ P ) )
46 44 45 syl5ibrcom 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 = P -> 4 <_ 2 ) )
47 2lt4 
 |-  2 < 4
48 2re 
 |-  2 e. RR
49 4re 
 |-  4 e. RR
50 48 49 ltnlei 
 |-  ( 2 < 4 <-> -. 4 <_ 2 )
51 47 50 mpbi 
 |-  -. 4 <_ 2
52 51 pm2.21i 
 |-  ( 4 <_ 2 -> ( P mod 6 ) e. { 1 , 5 } )
53 46 52 syl6 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 = P -> ( P mod 6 ) e. { 1 , 5 } ) )
54 43 53 sylbid 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 2 || ( P mod 6 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
55 breq2 
 |-  ( ( P mod 6 ) = M -> ( 2 || ( P mod 6 ) <-> 2 || M ) )
56 55 imbi1d 
 |-  ( ( P mod 6 ) = M -> ( ( 2 || ( P mod 6 ) -> ( P mod 6 ) e. { 1 , 5 } ) <-> ( 2 || M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
57 54 56 syl5ibcom 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( 2 || M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
58 57 com3r 
 |-  ( 2 || M -> ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
59 3nn 
 |-  3 e. NN
60 dvdsmul1 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> 3 || ( 3 x. 2 ) )
61 29 30 60 mp2an 
 |-  3 || ( 3 x. 2 )
62 61 33 breqtri 
 |-  3 || 6
63 dvdsmod 
 |-  ( ( ( 3 e. NN /\ 6 e. NN /\ P e. ZZ ) /\ 3 || 6 ) -> ( 3 || ( P mod 6 ) <-> 3 || P ) )
64 62 63 mpan2 
 |-  ( ( 3 e. NN /\ 6 e. NN /\ P e. ZZ ) -> ( 3 || ( P mod 6 ) <-> 3 || P ) )
65 59 26 28 64 mp3an12i 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 || ( P mod 6 ) <-> 3 || P ) )
66 df-3 
 |-  3 = ( 2 + 1 )
67 peano2uz 
 |-  ( 2 e. ( ZZ>= ` 2 ) -> ( 2 + 1 ) e. ( ZZ>= ` 2 ) )
68 39 67 ax-mp 
 |-  ( 2 + 1 ) e. ( ZZ>= ` 2 )
69 66 68 eqeltri 
 |-  3 e. ( ZZ>= ` 2 )
70 dvdsprm 
 |-  ( ( 3 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 3 || P <-> 3 = P ) )
71 69 40 70 sylancr 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 || P <-> 3 = P ) )
72 65 71 bitrd 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 || ( P mod 6 ) <-> 3 = P ) )
73 breq2 
 |-  ( 3 = P -> ( 4 <_ 3 <-> 4 <_ P ) )
74 44 73 syl5ibrcom 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 = P -> 4 <_ 3 ) )
75 3lt4 
 |-  3 < 4
76 3re 
 |-  3 e. RR
77 76 49 ltnlei 
 |-  ( 3 < 4 <-> -. 4 <_ 3 )
78 75 77 mpbi 
 |-  -. 4 <_ 3
79 78 pm2.21i 
 |-  ( 4 <_ 3 -> ( P mod 6 ) e. { 1 , 5 } )
80 74 79 syl6 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 = P -> ( P mod 6 ) e. { 1 , 5 } ) )
81 72 80 sylbid 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( 3 || ( P mod 6 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
82 breq2 
 |-  ( ( P mod 6 ) = M -> ( 3 || ( P mod 6 ) <-> 3 || M ) )
83 82 imbi1d 
 |-  ( ( P mod 6 ) = M -> ( ( 3 || ( P mod 6 ) -> ( P mod 6 ) e. { 1 , 5 } ) <-> ( 3 || M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
84 81 83 syl5ibcom 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( 3 || M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
85 84 com3r 
 |-  ( 3 || M -> ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
86 eleq1a 
 |-  ( M e. { 1 , 5 } -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) )
87 86 a1d 
 |-  ( M e. { 1 , 5 } -> ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
88 58 85 87 3jaoi 
 |-  ( ( 2 || M \/ 3 || M \/ M e. { 1 , 5 } ) -> ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) ) )
89 4 88 ax-mp 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) = M -> ( P mod 6 ) e. { 1 , 5 } ) )
90 3 oveq1i 
 |-  ( N ... 5 ) = ( ( M + 1 ) ... 5 )
91 90 eleq2i 
 |-  ( ( P mod 6 ) e. ( N ... 5 ) <-> ( P mod 6 ) e. ( ( M + 1 ) ... 5 ) )
92 1 simpri 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( N ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
93 91 92 syl5bir 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( ( M + 1 ) ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
94 89 93 jaod 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( ( P mod 6 ) = M \/ ( P mod 6 ) e. ( ( M + 1 ) ... 5 ) ) -> ( P mod 6 ) e. { 1 , 5 } ) )
95 24 94 syl5bi 
 |-  ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( M ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) )
96 17 95 pm3.2i 
 |-  ( M <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( M ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )