Metamath Proof Explorer

Theorem ppiub

Description: An upper bound on the prime-counting function ppi , which counts the number of primes less than N . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion ppiub 
|- ( ( N e. RR /\ 0 <_ N ) -> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) )

Proof

Step Hyp Ref Expression
1 3re 
 |-  3 e. RR
2 1 a1i 
 |-  ( ( N e. RR /\ 0 <_ N ) -> 3 e. RR )
3 simpl 
 |-  ( ( N e. RR /\ 0 <_ N ) -> N e. RR )
4 ppicl 
 |-  ( N e. RR -> ( ppi ` N ) e. NN0 )
5 4 nn0red 
 |-  ( N e. RR -> ( ppi ` N ) e. RR )
6 5 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ppi ` N ) e. RR )
7 2re 
 |-  2 e. RR
8 resubcl 
 |-  ( ( ( ppi ` N ) e. RR /\ 2 e. RR ) -> ( ( ppi ` N ) - 2 ) e. RR )
9 6 7 8 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` N ) - 2 ) e. RR )
10 fzfi 
 |-  ( 4 ... ( |_ ` N ) ) e. Fin
11 ssrab2 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } C_ ( 4 ... ( |_ ` N ) )
12 ssfi 
 |-  ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } C_ ( 4 ... ( |_ ` N ) ) ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin )
13 10 11 12 mp2an 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin
14 hashcl 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. NN0 )
15 13 14 ax-mp 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. NN0
16 15 nn0rei 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. RR
17 16 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. RR )
18 3nn 
 |-  3 e. NN
19 nndivre 
 |-  ( ( N e. RR /\ 3 e. NN ) -> ( N / 3 ) e. RR )
20 18 19 mpan2 
 |-  ( N e. RR -> ( N / 3 ) e. RR )
21 20 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N / 3 ) e. RR )
22 ppifl 
 |-  ( N e. RR -> ( ppi ` ( |_ ` N ) ) = ( ppi ` N ) )
23 22 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ppi ` ( |_ ` N ) ) = ( ppi ` N ) )
24 ppi3 
 |-  ( ppi ` 3 ) = 2
25 24 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ppi ` 3 ) = 2 )
26 23 25 oveq12d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` 3 ) ) = ( ( ppi ` N ) - 2 ) )
27 3z 
 |-  3 e. ZZ
28 27 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 3 e. ZZ )
29 flcl 
 |-  ( N e. RR -> ( |_ ` N ) e. ZZ )
30 29 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` N ) e. ZZ )
31 flge 
 |-  ( ( N e. RR /\ 3 e. ZZ ) -> ( 3 <_ N <-> 3 <_ ( |_ ` N ) ) )
32 27 31 mpan2 
 |-  ( N e. RR -> ( 3 <_ N <-> 3 <_ ( |_ ` N ) ) )
33 32 biimpa 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 3 <_ ( |_ ` N ) )
34 eluz2 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ ( |_ ` N ) e. ZZ /\ 3 <_ ( |_ ` N ) ) )
35 28 30 33 34 syl3anbrc 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` N ) e. ( ZZ>= ` 3 ) )
36 ppidif 
 |-  ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` 3 ) ) = ( # ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
37 35 36 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` 3 ) ) = ( # ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
38 df-4 
 |-  4 = ( 3 + 1 )
39 38 oveq1i 
 |-  ( 4 ... ( |_ ` N ) ) = ( ( 3 + 1 ) ... ( |_ ` N ) )
40 39 ineq1i 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) = ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime )
41 40 fveq2i 
 |-  ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) = ( # ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) )
42 37 41 eqtr4di 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` 3 ) ) = ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) )
43 26 42 eqtr3d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` N ) - 2 ) = ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) )
44 dfin5 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) = { k e. ( 4 ... ( |_ ` N ) ) | k e. Prime }
45 elfzle1 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> 4 <_ k )
46 ppiublem2 
 |-  ( ( k e. Prime /\ 4 <_ k ) -> ( k mod 6 ) e. { 1 , 5 } )
47 46 expcom 
 |-  ( 4 <_ k -> ( k e. Prime -> ( k mod 6 ) e. { 1 , 5 } ) )
48 45 47 syl 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> ( k e. Prime -> ( k mod 6 ) e. { 1 , 5 } ) )
49 48 ss2rabi 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | k e. Prime } C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } }
50 44 49 eqsstri 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } }
51 ssdomg 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin -> ( ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
52 13 50 51 mp2 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } }
53 inss1 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ ( 4 ... ( |_ ` N ) )
54 ssfi 
 |-  ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ ( 4 ... ( |_ ` N ) ) ) -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin )
55 10 53 54 mp2an 
 |-  ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin
56 hashdom 
 |-  ( ( ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin ) -> ( ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <-> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
57 55 13 56 mp2an 
 |-  ( ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <-> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } )
58 52 57 mpbir 
 |-  ( # ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } )
59 43 58 eqbrtrdi 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` N ) - 2 ) <_ ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
60 reflcl 
 |-  ( N e. RR -> ( |_ ` N ) e. RR )
61 60 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` N ) e. RR )
62 peano2rem 
 |-  ( ( |_ ` N ) e. RR -> ( ( |_ ` N ) - 1 ) e. RR )
63 61 62 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` N ) - 1 ) e. RR )
64 6nn 
 |-  6 e. NN
65 nndivre 
 |-  ( ( ( ( |_ ` N ) - 1 ) e. RR /\ 6 e. NN ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR )
66 63 64 65 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR )
67 reflcl 
 |-  ( ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. RR )
68 66 67 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. RR )
69 5re 
 |-  5 e. RR
70 resubcl 
 |-  ( ( ( |_ ` N ) e. RR /\ 5 e. RR ) -> ( ( |_ ` N ) - 5 ) e. RR )
71 61 69 70 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` N ) - 5 ) e. RR )
72 nndivre 
 |-  ( ( ( ( |_ ` N ) - 5 ) e. RR /\ 6 e. NN ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR )
73 71 64 72 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR )
74 reflcl 
 |-  ( ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. RR )
75 73 74 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. RR )
76 peano2re 
 |-  ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. RR -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) e. RR )
77 75 76 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) e. RR )
78 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
79 78 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N - 1 ) e. RR )
80 nndivre 
 |-  ( ( ( N - 1 ) e. RR /\ 6 e. NN ) -> ( ( N - 1 ) / 6 ) e. RR )
81 79 64 80 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N - 1 ) / 6 ) e. RR )
82 simpl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> N e. RR )
83 resubcl 
 |-  ( ( N e. RR /\ 5 e. RR ) -> ( N - 5 ) e. RR )
84 82 69 83 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N - 5 ) e. RR )
85 nndivre 
 |-  ( ( ( N - 5 ) e. RR /\ 6 e. NN ) -> ( ( N - 5 ) / 6 ) e. RR )
86 84 64 85 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N - 5 ) / 6 ) e. RR )
87 peano2re 
 |-  ( ( ( N - 5 ) / 6 ) e. RR -> ( ( ( N - 5 ) / 6 ) + 1 ) e. RR )
88 86 87 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( N - 5 ) / 6 ) + 1 ) e. RR )
89 flle 
 |-  ( ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 1 ) / 6 ) )
90 66 89 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 1 ) / 6 ) )
91 1re 
 |-  1 e. RR
92 91 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 1 e. RR )
93 flle 
 |-  ( N e. RR -> ( |_ ` N ) <_ N )
94 93 adantr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` N ) <_ N )
95 61 82 92 94 lesub1dd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) )
96 6re 
 |-  6 e. RR
97 96 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 6 e. RR )
98 6pos 
 |-  0 < 6
99 98 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 0 < 6 )
100 lediv1 
 |-  ( ( ( ( |_ ` N ) - 1 ) e. RR /\ ( N - 1 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) <-> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) ) )
101 63 79 97 99 100 syl112anc 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) <-> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) ) )
102 95 101 mpbid 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) )
103 68 66 81 90 102 letrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( N - 1 ) / 6 ) )
104 flle 
 |-  ( ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 5 ) / 6 ) )
105 73 104 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 5 ) / 6 ) )
106 69 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 5 e. RR )
107 61 82 106 94 lesub1dd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) )
108 lediv1 
 |-  ( ( ( ( |_ ` N ) - 5 ) e. RR /\ ( N - 5 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) <-> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) ) )
109 71 84 97 99 108 syl112anc 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) <-> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) ) )
110 107 109 mpbid 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) )
111 75 73 86 105 110 letrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( N - 5 ) / 6 ) )
112 75 86 92 111 leadd1dd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) <_ ( ( ( N - 5 ) / 6 ) + 1 ) )
113 68 77 81 88 103 112 le2addd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) <_ ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
114 ovex 
 |-  ( k mod 6 ) e. _V
115 114 elpr 
 |-  ( ( k mod 6 ) e. { 1 , 5 } <-> ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) )
116 115 rabbii 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) }
117 unrab 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) }
118 116 117 eqtr4i 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } = ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } )
119 118 fveq2i 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( # ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) )
120 ssrab2 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } C_ ( 4 ... ( |_ ` N ) )
121 ssfi 
 |-  ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } C_ ( 4 ... ( |_ ` N ) ) ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin )
122 10 120 121 mp2an 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin
123 ssrab2 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } C_ ( 4 ... ( |_ ` N ) )
124 ssfi 
 |-  ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } C_ ( 4 ... ( |_ ` N ) ) ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin )
125 10 123 124 mp2an 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin
126 inrab 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) }
127 rabeq0 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) } = (/) <-> A. k e. ( 4 ... ( |_ ` N ) ) -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
128 1lt5 
 |-  1 < 5
129 91 128 ltneii 
 |-  1 =/= 5
130 eqtr2 
 |-  ( ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) -> 1 = 5 )
131 130 necon3ai 
 |-  ( 1 =/= 5 -> -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
132 129 131 ax-mp 
 |-  -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 )
133 132 a1i 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
134 127 133 mprgbir 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) } = (/)
135 126 134 eqtri 
 |-  ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (/)
136 hashun 
 |-  ( ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin /\ ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (/) ) -> ( # ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) )
137 122 125 135 136 mp3an 
 |-  ( # ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) )
138 119 137 eqtri 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) )
139 elfzelz 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> k e. ZZ )
140 nnrp 
 |-  ( 6 e. NN -> 6 e. RR+ )
141 64 140 ax-mp 
 |-  6 e. RR+
142 0le1 
 |-  0 <_ 1
143 1lt6 
 |-  1 < 6
144 modid 
 |-  ( ( ( 1 e. RR /\ 6 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 6 ) ) -> ( 1 mod 6 ) = 1 )
145 91 141 142 143 144 mp4an 
 |-  ( 1 mod 6 ) = 1
146 145 eqeq2i 
 |-  ( ( k mod 6 ) = ( 1 mod 6 ) <-> ( k mod 6 ) = 1 )
147 1z 
 |-  1 e. ZZ
148 moddvds 
 |-  ( ( 6 e. NN /\ k e. ZZ /\ 1 e. ZZ ) -> ( ( k mod 6 ) = ( 1 mod 6 ) <-> 6 || ( k - 1 ) ) )
149 64 147 148 mp3an13 
 |-  ( k e. ZZ -> ( ( k mod 6 ) = ( 1 mod 6 ) <-> 6 || ( k - 1 ) ) )
150 146 149 bitr3id 
 |-  ( k e. ZZ -> ( ( k mod 6 ) = 1 <-> 6 || ( k - 1 ) ) )
151 139 150 syl 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> ( ( k mod 6 ) = 1 <-> 6 || ( k - 1 ) ) )
152 151 rabbiia 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } = { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) }
153 152 fveq2i 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = ( # ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) } )
154 64 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 6 e. NN )
155 4z 
 |-  4 e. ZZ
156 155 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 4 e. ZZ )
157 4m1e3 
 |-  ( 4 - 1 ) = 3
158 157 fveq2i 
 |-  ( ZZ>= ` ( 4 - 1 ) ) = ( ZZ>= ` 3 )
159 35 158 eleqtrrdi 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` N ) e. ( ZZ>= ` ( 4 - 1 ) ) )
160 147 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 1 e. ZZ )
161 154 156 159 160 hashdvds 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) )
162 153 161 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) )
163 2cn 
 |-  2 e. CC
164 ax-1cn 
 |-  1 e. CC
165 df-3 
 |-  3 = ( 2 + 1 )
166 157 165 eqtri 
 |-  ( 4 - 1 ) = ( 2 + 1 )
167 163 164 166 mvrraddi 
 |-  ( ( 4 - 1 ) - 1 ) = 2
168 167 oveq1i 
 |-  ( ( ( 4 - 1 ) - 1 ) / 6 ) = ( 2 / 6 )
169 168 fveq2i 
 |-  ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) = ( |_ ` ( 2 / 6 ) )
170 0re 
 |-  0 e. RR
171 64 nnne0i 
 |-  6 =/= 0
172 7 96 171 redivcli 
 |-  ( 2 / 6 ) e. RR
173 2pos 
 |-  0 < 2
174 7 96 173 98 divgt0ii 
 |-  0 < ( 2 / 6 )
175 170 172 174 ltleii 
 |-  0 <_ ( 2 / 6 )
176 2lt6 
 |-  2 < 6
177 6cn 
 |-  6 e. CC
178 177 mulid1i 
 |-  ( 6 x. 1 ) = 6
179 176 178 breqtrri 
 |-  2 < ( 6 x. 1 )
180 96 98 pm3.2i 
 |-  ( 6 e. RR /\ 0 < 6 )
181 ltdivmul 
 |-  ( ( 2 e. RR /\ 1 e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( 2 / 6 ) < 1 <-> 2 < ( 6 x. 1 ) ) )
182 7 91 180 181 mp3an 
 |-  ( ( 2 / 6 ) < 1 <-> 2 < ( 6 x. 1 ) )
183 179 182 mpbir 
 |-  ( 2 / 6 ) < 1
184 1e0p1 
 |-  1 = ( 0 + 1 )
185 183 184 breqtri 
 |-  ( 2 / 6 ) < ( 0 + 1 )
186 0z 
 |-  0 e. ZZ
187 flbi 
 |-  ( ( ( 2 / 6 ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( 2 / 6 ) ) = 0 <-> ( 0 <_ ( 2 / 6 ) /\ ( 2 / 6 ) < ( 0 + 1 ) ) ) )
188 172 186 187 mp2an 
 |-  ( ( |_ ` ( 2 / 6 ) ) = 0 <-> ( 0 <_ ( 2 / 6 ) /\ ( 2 / 6 ) < ( 0 + 1 ) ) )
189 175 185 188 mpbir2an 
 |-  ( |_ ` ( 2 / 6 ) ) = 0
190 169 189 eqtri 
 |-  ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) = 0
191 190 oveq2i 
 |-  ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - 0 )
192 66 flcld 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. ZZ )
193 192 zcnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. CC )
194 193 subid1d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - 0 ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
195 191 194 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
196 162 195 eqtrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
197 5pos 
 |-  0 < 5
198 170 69 197 ltleii 
 |-  0 <_ 5
199 5lt6 
 |-  5 < 6
200 modid 
 |-  ( ( ( 5 e. RR /\ 6 e. RR+ ) /\ ( 0 <_ 5 /\ 5 < 6 ) ) -> ( 5 mod 6 ) = 5 )
201 69 141 198 199 200 mp4an 
 |-  ( 5 mod 6 ) = 5
202 201 eqeq2i 
 |-  ( ( k mod 6 ) = ( 5 mod 6 ) <-> ( k mod 6 ) = 5 )
203 5nn 
 |-  5 e. NN
204 203 nnzi 
 |-  5 e. ZZ
205 moddvds 
 |-  ( ( 6 e. NN /\ k e. ZZ /\ 5 e. ZZ ) -> ( ( k mod 6 ) = ( 5 mod 6 ) <-> 6 || ( k - 5 ) ) )
206 64 204 205 mp3an13 
 |-  ( k e. ZZ -> ( ( k mod 6 ) = ( 5 mod 6 ) <-> 6 || ( k - 5 ) ) )
207 202 206 bitr3id 
 |-  ( k e. ZZ -> ( ( k mod 6 ) = 5 <-> 6 || ( k - 5 ) ) )
208 139 207 syl 
 |-  ( k e. ( 4 ... ( |_ ` N ) ) -> ( ( k mod 6 ) = 5 <-> 6 || ( k - 5 ) ) )
209 208 rabbiia 
 |-  { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } = { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) }
210 209 fveq2i 
 |-  ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = ( # ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) } )
211 204 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 5 e. ZZ )
212 154 156 159 211 hashdvds 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) )
213 210 212 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) )
214 157 oveq1i 
 |-  ( ( 4 - 1 ) - 5 ) = ( 3 - 5 )
215 5cn 
 |-  5 e. CC
216 3cn 
 |-  3 e. CC
217 215 216 negsubdi2i 
 |-  -u ( 5 - 3 ) = ( 3 - 5 )
218 3p2e5 
 |-  ( 3 + 2 ) = 5
219 218 oveq1i 
 |-  ( ( 3 + 2 ) - 3 ) = ( 5 - 3 )
220 pncan2 
 |-  ( ( 3 e. CC /\ 2 e. CC ) -> ( ( 3 + 2 ) - 3 ) = 2 )
221 216 163 220 mp2an 
 |-  ( ( 3 + 2 ) - 3 ) = 2
222 219 221 eqtr3i 
 |-  ( 5 - 3 ) = 2
223 222 negeqi 
 |-  -u ( 5 - 3 ) = -u 2
224 214 217 223 3eqtr2i 
 |-  ( ( 4 - 1 ) - 5 ) = -u 2
225 224 oveq1i 
 |-  ( ( ( 4 - 1 ) - 5 ) / 6 ) = ( -u 2 / 6 )
226 divneg 
 |-  ( ( 2 e. CC /\ 6 e. CC /\ 6 =/= 0 ) -> -u ( 2 / 6 ) = ( -u 2 / 6 ) )
227 163 177 171 226 mp3an 
 |-  -u ( 2 / 6 ) = ( -u 2 / 6 )
228 225 227 eqtr4i 
 |-  ( ( ( 4 - 1 ) - 5 ) / 6 ) = -u ( 2 / 6 )
229 228 fveq2i 
 |-  ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) = ( |_ ` -u ( 2 / 6 ) )
230 172 91 183 ltleii 
 |-  ( 2 / 6 ) <_ 1
231 172 91 lenegi 
 |-  ( ( 2 / 6 ) <_ 1 <-> -u 1 <_ -u ( 2 / 6 ) )
232 230 231 mpbi 
 |-  -u 1 <_ -u ( 2 / 6 )
233 170 172 ltnegi 
 |-  ( 0 < ( 2 / 6 ) <-> -u ( 2 / 6 ) < -u 0 )
234 174 233 mpbi 
 |-  -u ( 2 / 6 ) < -u 0
235 neg0 
 |-  -u 0 = 0
236 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
237 235 236 eqtr4i 
 |-  -u 0 = ( 1 + -u 1 )
238 neg1cn 
 |-  -u 1 e. CC
239 238 164 addcomi 
 |-  ( -u 1 + 1 ) = ( 1 + -u 1 )
240 237 239 eqtr4i 
 |-  -u 0 = ( -u 1 + 1 )
241 234 240 breqtri 
 |-  -u ( 2 / 6 ) < ( -u 1 + 1 )
242 172 renegcli 
 |-  -u ( 2 / 6 ) e. RR
243 neg1z 
 |-  -u 1 e. ZZ
244 flbi 
 |-  ( ( -u ( 2 / 6 ) e. RR /\ -u 1 e. ZZ ) -> ( ( |_ ` -u ( 2 / 6 ) ) = -u 1 <-> ( -u 1 <_ -u ( 2 / 6 ) /\ -u ( 2 / 6 ) < ( -u 1 + 1 ) ) ) )
245 242 243 244 mp2an 
 |-  ( ( |_ ` -u ( 2 / 6 ) ) = -u 1 <-> ( -u 1 <_ -u ( 2 / 6 ) /\ -u ( 2 / 6 ) < ( -u 1 + 1 ) ) )
246 232 241 245 mpbir2an 
 |-  ( |_ ` -u ( 2 / 6 ) ) = -u 1
247 229 246 eqtri 
 |-  ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) = -u 1
248 247 oveq2i 
 |-  ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 )
249 73 flcld 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. ZZ )
250 249 zcnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. CC )
251 subneg 
 |-  ( ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. CC /\ 1 e. CC ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
252 250 164 251 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
253 248 252 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
254 213 253 eqtrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
255 196 254 oveq12d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) )
256 138 255 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) )
257 82 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> N e. CC )
258 257 2timesd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( 2 x. N ) = ( N + N ) )
259 df-6 
 |-  6 = ( 5 + 1 )
260 215 164 addcomi 
 |-  ( 5 + 1 ) = ( 1 + 5 )
261 259 260 eqtri 
 |-  6 = ( 1 + 5 )
262 261 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 6 = ( 1 + 5 ) )
263 258 262 oveq12d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( 2 x. N ) - 6 ) = ( ( N + N ) - ( 1 + 5 ) ) )
264 addsub4 
 |-  ( ( ( N e. CC /\ N e. CC ) /\ ( 1 e. CC /\ 5 e. CC ) ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
265 164 215 264 mpanr12 
 |-  ( ( N e. CC /\ N e. CC ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
266 257 257 265 syl2anc 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
267 263 266 eqtrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( 2 x. N ) - 6 ) = ( ( N - 1 ) + ( N - 5 ) ) )
268 267 oveq1d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) )
269 mulcl 
 |-  ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) e. CC )
270 163 257 269 sylancr 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( 2 x. N ) e. CC )
271 177 171 pm3.2i 
 |-  ( 6 e. CC /\ 6 =/= 0 )
272 divsubdir 
 |-  ( ( ( 2 x. N ) e. CC /\ 6 e. CC /\ ( 6 e. CC /\ 6 =/= 0 ) ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
273 177 271 272 mp3an23 
 |-  ( ( 2 x. N ) e. CC -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
274 270 273 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
275 3t2e6 
 |-  ( 3 x. 2 ) = 6
276 216 163 mulcomi 
 |-  ( 3 x. 2 ) = ( 2 x. 3 )
277 275 276 eqtr3i 
 |-  6 = ( 2 x. 3 )
278 277 oveq2i 
 |-  ( ( 2 x. N ) / 6 ) = ( ( 2 x. N ) / ( 2 x. 3 ) )
279 3ne0 
 |-  3 =/= 0
280 216 279 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
281 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
282 divcan5 
 |-  ( ( N e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
283 280 281 282 mp3an23 
 |-  ( N e. CC -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
284 257 283 syl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
285 278 284 syl5eq 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( 2 x. N ) / 6 ) = ( N / 3 ) )
286 177 171 dividi 
 |-  ( 6 / 6 ) = 1
287 286 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( 6 / 6 ) = 1 )
288 285 287 oveq12d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) = ( ( N / 3 ) - 1 ) )
289 274 288 eqtrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( N / 3 ) - 1 ) )
290 79 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N - 1 ) e. CC )
291 84 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N - 5 ) e. CC )
292 divdir 
 |-  ( ( ( N - 1 ) e. CC /\ ( N - 5 ) e. CC /\ ( 6 e. CC /\ 6 =/= 0 ) ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
293 271 292 mp3an3 
 |-  ( ( ( N - 1 ) e. CC /\ ( N - 5 ) e. CC ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
294 290 291 293 syl2anc 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
295 268 289 294 3eqtr3d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N / 3 ) - 1 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
296 295 oveq1d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) + 1 ) )
297 21 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N / 3 ) e. CC )
298 npcan 
 |-  ( ( ( N / 3 ) e. CC /\ 1 e. CC ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( N / 3 ) )
299 297 164 298 sylancl 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( N / 3 ) )
300 81 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N - 1 ) / 6 ) e. CC )
301 86 recnd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( N - 5 ) / 6 ) e. CC )
302 164 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 1 e. CC )
303 300 301 302 addassd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) + 1 ) = ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
304 296 299 303 3eqtr3d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( N / 3 ) = ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
305 113 256 304 3brtr4d 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( # ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <_ ( N / 3 ) )
306 9 17 21 59 305 letrd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ppi ` N ) - 2 ) <_ ( N / 3 ) )
307 7 a1i 
 |-  ( ( N e. RR /\ 3 <_ N ) -> 2 e. RR )
308 6 307 21 lesubaddd 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ( ( ppi ` N ) - 2 ) <_ ( N / 3 ) <-> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) ) )
309 306 308 mpbid 
 |-  ( ( N e. RR /\ 3 <_ N ) -> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) )
310 309 adantlr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ 3 <_ N ) -> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) )
311 5 ad2antrr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( ppi ` N ) e. RR )
312 7 a1i 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> 2 e. RR )
313 20 ad2antrr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( N / 3 ) e. RR )
314 readdcl 
 |-  ( ( ( N / 3 ) e. RR /\ 2 e. RR ) -> ( ( N / 3 ) + 2 ) e. RR )
315 313 7 314 sylancl 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( ( N / 3 ) + 2 ) e. RR )
316 ppiwordi 
 |-  ( ( N e. RR /\ 3 e. RR /\ N <_ 3 ) -> ( ppi ` N ) <_ ( ppi ` 3 ) )
317 1 316 mp3an2 
 |-  ( ( N e. RR /\ N <_ 3 ) -> ( ppi ` N ) <_ ( ppi ` 3 ) )
318 317 adantlr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( ppi ` N ) <_ ( ppi ` 3 ) )
319 318 24 breqtrdi 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( ppi ` N ) <_ 2 )
320 3pos 
 |-  0 < 3
321 divge0 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ ( 3 e. RR /\ 0 < 3 ) ) -> 0 <_ ( N / 3 ) )
322 1 320 321 mpanr12 
 |-  ( ( N e. RR /\ 0 <_ N ) -> 0 <_ ( N / 3 ) )
323 322 adantr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> 0 <_ ( N / 3 ) )
324 addge02 
 |-  ( ( 2 e. RR /\ ( N / 3 ) e. RR ) -> ( 0 <_ ( N / 3 ) <-> 2 <_ ( ( N / 3 ) + 2 ) ) )
325 7 313 324 sylancr 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( 0 <_ ( N / 3 ) <-> 2 <_ ( ( N / 3 ) + 2 ) ) )
326 323 325 mpbid 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> 2 <_ ( ( N / 3 ) + 2 ) )
327 311 312 315 319 326 letrd 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ N <_ 3 ) -> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) )
328 2 3 310 327 lecasei 
 |-  ( ( N e. RR /\ 0 <_ N ) -> ( ppi ` N ) <_ ( ( N / 3 ) + 2 ) )