Metamath Proof Explorer

Theorem prmreclem5

Description: Lemma for prmrec . Here we show the inequality N / 2 < # M by decomposing the set ( 1 ... N ) into the disjoint union of the set M of those numbers that are not divisible by any "large" primes (above K ) and the indexed union over K < k of the numbers Wk that divide the prime k . By prmreclem4 the second of these has size less than N times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part M must be at least N / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses prmrec.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
prmrec.2 
|- ( ph -> K e. NN )
prmrec.3 
|- ( ph -> N e. NN )
prmrec.4 
|- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }
prmrec.5 
|- ( ph -> seq 1 ( + , F ) e. dom ~~> )
prmrec.6 
|- ( ph -> sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) )
prmrec.7 
|- W = ( p e. NN |-> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } )
Assertion prmreclem5 
|- ( ph -> ( N / 2 ) < ( ( 2 ^ K ) x. ( sqrt ` N ) ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
2 prmrec.2 
 |-  ( ph -> K e. NN )
3 prmrec.3 
 |-  ( ph -> N e. NN )
4 prmrec.4 
 |-  M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }
5 prmrec.5 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )
6 prmrec.6 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) )
7 prmrec.7 
 |-  W = ( p e. NN |-> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } )
8 3 nnred 
 |-  ( ph -> N e. RR )
9 8 rehalfcld 
 |-  ( ph -> ( N / 2 ) e. RR )
10 fzfi 
 |-  ( 1 ... N ) e. Fin
11 4 ssrab3 
 |-  M C_ ( 1 ... N )
12 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ M C_ ( 1 ... N ) ) -> M e. Fin )
13 10 11 12 mp2an 
 |-  M e. Fin
14 hashcl 
 |-  ( M e. Fin -> ( # ` M ) e. NN0 )
15 13 14 ax-mp 
 |-  ( # ` M ) e. NN0
16 15 nn0rei 
 |-  ( # ` M ) e. RR
17 16 a1i 
 |-  ( ph -> ( # ` M ) e. RR )
18 2nn 
 |-  2 e. NN
19 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
20 nnexpcl 
 |-  ( ( 2 e. NN /\ K e. NN0 ) -> ( 2 ^ K ) e. NN )
21 18 19 20 sylancr 
 |-  ( ph -> ( 2 ^ K ) e. NN )
22 21 nnred 
 |-  ( ph -> ( 2 ^ K ) e. RR )
23 3 nnrpd 
 |-  ( ph -> N e. RR+ )
24 23 rpsqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR+ )
25 24 rpred 
 |-  ( ph -> ( sqrt ` N ) e. RR )
26 22 25 remulcld 
 |-  ( ph -> ( ( 2 ^ K ) x. ( sqrt ` N ) ) e. RR )
27 8 recnd 
 |-  ( ph -> N e. CC )
28 27 2halvesd 
 |-  ( ph -> ( ( N / 2 ) + ( N / 2 ) ) = N )
29 11 a1i 
 |-  ( ph -> M C_ ( 1 ... N ) )
30 2 peano2nnd 
 |-  ( ph -> ( K + 1 ) e. NN )
31 elfzuz 
 |-  ( k e. ( ( K + 1 ) ... N ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
32 eluznn 
 |-  ( ( ( K + 1 ) e. NN /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN )
33 30 31 32 syl2an 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> k e. NN )
34 eleq1w 
 |-  ( p = k -> ( p e. Prime <-> k e. Prime ) )
35 breq1 
 |-  ( p = k -> ( p || n <-> k || n ) )
36 34 35 anbi12d 
 |-  ( p = k -> ( ( p e. Prime /\ p || n ) <-> ( k e. Prime /\ k || n ) ) )
37 36 rabbidv 
 |-  ( p = k -> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
38 ovex 
 |-  ( 1 ... N ) e. _V
39 38 rabex 
 |-  { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } e. _V
40 37 7 39 fvmpt 
 |-  ( k e. NN -> ( W ` k ) = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
41 40 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( W ` k ) = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
42 ssrab2 
 |-  { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } C_ ( 1 ... N )
43 41 42 eqsstrdi 
 |-  ( ( ph /\ k e. NN ) -> ( W ` k ) C_ ( 1 ... N ) )
44 33 43 syldan 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( W ` k ) C_ ( 1 ... N ) )
45 44 ralrimiva 
 |-  ( ph -> A. k e. ( ( K + 1 ) ... N ) ( W ` k ) C_ ( 1 ... N ) )
46 iunss 
 |-  ( U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) C_ ( 1 ... N ) <-> A. k e. ( ( K + 1 ) ... N ) ( W ` k ) C_ ( 1 ... N ) )
47 45 46 sylibr 
 |-  ( ph -> U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) C_ ( 1 ... N ) )
48 29 47 unssd 
 |-  ( ph -> ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) C_ ( 1 ... N ) )
49 breq1 
 |-  ( p = q -> ( p || n <-> q || n ) )
50 49 notbid 
 |-  ( p = q -> ( -. p || n <-> -. q || n ) )
51 50 cbvralvw 
 |-  ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. q e. ( Prime \ ( 1 ... K ) ) -. q || n )
52 breq2 
 |-  ( n = x -> ( q || n <-> q || x ) )
53 52 notbid 
 |-  ( n = x -> ( -. q || n <-> -. q || x ) )
54 53 ralbidv 
 |-  ( n = x -> ( A. q e. ( Prime \ ( 1 ... K ) ) -. q || n <-> A. q e. ( Prime \ ( 1 ... K ) ) -. q || x ) )
55 51 54 syl5bb 
 |-  ( n = x -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. q e. ( Prime \ ( 1 ... K ) ) -. q || x ) )
56 55 4 elrab2 
 |-  ( x e. M <-> ( x e. ( 1 ... N ) /\ A. q e. ( Prime \ ( 1 ... K ) ) -. q || x ) )
57 elun1 
 |-  ( x e. M -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
58 56 57 sylbir 
 |-  ( ( x e. ( 1 ... N ) /\ A. q e. ( Prime \ ( 1 ... K ) ) -. q || x ) -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
59 58 ex 
 |-  ( x e. ( 1 ... N ) -> ( A. q e. ( Prime \ ( 1 ... K ) ) -. q || x -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
60 59 adantl 
 |-  ( ( ph /\ x e. ( 1 ... N ) ) -> ( A. q e. ( Prime \ ( 1 ... K ) ) -. q || x -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
61 dfrex2 
 |-  ( E. q e. ( Prime \ ( 1 ... K ) ) q || x <-> -. A. q e. ( Prime \ ( 1 ... K ) ) -. q || x )
62 eldifn 
 |-  ( q e. ( Prime \ ( 1 ... K ) ) -> -. q e. ( 1 ... K ) )
63 62 ad2antrl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> -. q e. ( 1 ... K ) )
64 eldifi 
 |-  ( q e. ( Prime \ ( 1 ... K ) ) -> q e. Prime )
65 64 ad2antrl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. Prime )
66 prmnn 
 |-  ( q e. Prime -> q e. NN )
67 65 66 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. NN )
68 nnuz 
 |-  NN = ( ZZ>= ` 1 )
69 67 68 eleqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. ( ZZ>= ` 1 ) )
70 2 nnzd 
 |-  ( ph -> K e. ZZ )
71 70 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> K e. ZZ )
72 elfz5 
 |-  ( ( q e. ( ZZ>= ` 1 ) /\ K e. ZZ ) -> ( q e. ( 1 ... K ) <-> q <_ K ) )
73 69 71 72 syl2anc 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( q e. ( 1 ... K ) <-> q <_ K ) )
74 63 73 mtbid 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> -. q <_ K )
75 2 nnred 
 |-  ( ph -> K e. RR )
76 75 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> K e. RR )
77 67 nnred 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. RR )
78 76 77 ltnled 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( K < q <-> -. q <_ K ) )
79 74 78 mpbird 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> K < q )
80 prmz 
 |-  ( q e. Prime -> q e. ZZ )
81 65 80 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. ZZ )
82 zltp1le 
 |-  ( ( K e. ZZ /\ q e. ZZ ) -> ( K < q <-> ( K + 1 ) <_ q ) )
83 71 81 82 syl2anc 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( K < q <-> ( K + 1 ) <_ q ) )
84 79 83 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( K + 1 ) <_ q )
85 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
86 85 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. NN )
87 86 nnred 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. RR )
88 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> N e. RR )
89 simprr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q || x )
90 dvdsle 
 |-  ( ( q e. ZZ /\ x e. NN ) -> ( q || x -> q <_ x ) )
91 81 86 90 syl2anc 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( q || x -> q <_ x ) )
92 89 91 mpd 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q <_ x )
93 elfzle2 
 |-  ( x e. ( 1 ... N ) -> x <_ N )
94 93 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x <_ N )
95 77 87 88 92 94 letrd 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q <_ N )
96 70 peano2zd 
 |-  ( ph -> ( K + 1 ) e. ZZ )
97 96 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( K + 1 ) e. ZZ )
98 3 nnzd 
 |-  ( ph -> N e. ZZ )
99 98 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> N e. ZZ )
100 elfz 
 |-  ( ( q e. ZZ /\ ( K + 1 ) e. ZZ /\ N e. ZZ ) -> ( q e. ( ( K + 1 ) ... N ) <-> ( ( K + 1 ) <_ q /\ q <_ N ) ) )
101 81 97 99 100 syl3anc 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( q e. ( ( K + 1 ) ... N ) <-> ( ( K + 1 ) <_ q /\ q <_ N ) ) )
102 84 95 101 mpbir2and 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> q e. ( ( K + 1 ) ... N ) )
103 52 anbi2d 
 |-  ( n = x -> ( ( q e. Prime /\ q || n ) <-> ( q e. Prime /\ q || x ) ) )
104 simplr 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. ( 1 ... N ) )
105 65 89 jca 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( q e. Prime /\ q || x ) )
106 103 104 105 elrabd 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. { n e. ( 1 ... N ) | ( q e. Prime /\ q || n ) } )
107 eleq1w 
 |-  ( p = q -> ( p e. Prime <-> q e. Prime ) )
108 107 49 anbi12d 
 |-  ( p = q -> ( ( p e. Prime /\ p || n ) <-> ( q e. Prime /\ q || n ) ) )
109 108 rabbidv 
 |-  ( p = q -> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } = { n e. ( 1 ... N ) | ( q e. Prime /\ q || n ) } )
110 38 rabex 
 |-  { n e. ( 1 ... N ) | ( q e. Prime /\ q || n ) } e. _V
111 109 7 110 fvmpt 
 |-  ( q e. NN -> ( W ` q ) = { n e. ( 1 ... N ) | ( q e. Prime /\ q || n ) } )
112 67 111 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> ( W ` q ) = { n e. ( 1 ... N ) | ( q e. Prime /\ q || n ) } )
113 106 112 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. ( W ` q ) )
114 fveq2 
 |-  ( k = q -> ( W ` k ) = ( W ` q ) )
115 114 eliuni 
 |-  ( ( q e. ( ( K + 1 ) ... N ) /\ x e. ( W ` q ) ) -> x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) )
116 102 113 115 syl2anc 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) )
117 elun2 
 |-  ( x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
118 116 117 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... N ) ) /\ ( q e. ( Prime \ ( 1 ... K ) ) /\ q || x ) ) -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
119 118 rexlimdvaa 
 |-  ( ( ph /\ x e. ( 1 ... N ) ) -> ( E. q e. ( Prime \ ( 1 ... K ) ) q || x -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
120 61 119 syl5bir 
 |-  ( ( ph /\ x e. ( 1 ... N ) ) -> ( -. A. q e. ( Prime \ ( 1 ... K ) ) -. q || x -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
121 60 120 pm2.61d 
 |-  ( ( ph /\ x e. ( 1 ... N ) ) -> x e. ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
122 48 121 eqelssd 
 |-  ( ph -> ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) = ( 1 ... N ) )
123 122 fveq2d 
 |-  ( ph -> ( # ` ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) = ( # ` ( 1 ... N ) ) )
124 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
125 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
126 124 125 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
127 123 126 eqtr2d 
 |-  ( ph -> N = ( # ` ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
128 13 a1i 
 |-  ( ph -> M e. Fin )
129 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) C_ ( 1 ... N ) ) -> U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) e. Fin )
130 10 47 129 sylancr 
 |-  ( ph -> U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) e. Fin )
131 breq1 
 |-  ( p = k -> ( p || x <-> k || x ) )
132 131 notbid 
 |-  ( p = k -> ( -. p || x <-> -. k || x ) )
133 breq2 
 |-  ( n = x -> ( p || n <-> p || x ) )
134 133 notbid 
 |-  ( n = x -> ( -. p || n <-> -. p || x ) )
135 134 ralbidv 
 |-  ( n = x -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || x ) )
136 135 4 elrab2 
 |-  ( x e. M <-> ( x e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || x ) )
137 136 simprbi 
 |-  ( x e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || x )
138 137 ad2antlr 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || x )
139 simprr 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> k e. Prime )
140 noel 
 |-  -. k e. (/)
141 simprl 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> k e. ( ( K + 1 ) ... N ) )
142 141 biantrud 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> ( k e. ( 1 ... K ) <-> ( k e. ( 1 ... K ) /\ k e. ( ( K + 1 ) ... N ) ) ) )
143 elin 
 |-  ( k e. ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) <-> ( k e. ( 1 ... K ) /\ k e. ( ( K + 1 ) ... N ) ) )
144 142 143 bitr4di 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> ( k e. ( 1 ... K ) <-> k e. ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) ) )
145 75 ltp1d 
 |-  ( ph -> K < ( K + 1 ) )
146 fzdisj 
 |-  ( K < ( K + 1 ) -> ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) = (/) )
147 145 146 syl 
 |-  ( ph -> ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) = (/) )
148 147 ad2antrr 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) = (/) )
149 148 eleq2d 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> ( k e. ( ( 1 ... K ) i^i ( ( K + 1 ) ... N ) ) <-> k e. (/) ) )
150 144 149 bitrd 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> ( k e. ( 1 ... K ) <-> k e. (/) ) )
151 140 150 mtbiri 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> -. k e. ( 1 ... K ) )
152 139 151 eldifd 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> k e. ( Prime \ ( 1 ... K ) ) )
153 132 138 152 rspcdva 
 |-  ( ( ( ph /\ x e. M ) /\ ( k e. ( ( K + 1 ) ... N ) /\ k e. Prime ) ) -> -. k || x )
154 153 expr 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> ( k e. Prime -> -. k || x ) )
155 imnan 
 |-  ( ( k e. Prime -> -. k || x ) <-> -. ( k e. Prime /\ k || x ) )
156 154 155 sylib 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> -. ( k e. Prime /\ k || x ) )
157 33 adantlr 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> k e. NN )
158 157 40 syl 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> ( W ` k ) = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
159 158 eleq2d 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> ( x e. ( W ` k ) <-> x e. { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } ) )
160 breq2 
 |-  ( n = x -> ( k || n <-> k || x ) )
161 160 anbi2d 
 |-  ( n = x -> ( ( k e. Prime /\ k || n ) <-> ( k e. Prime /\ k || x ) ) )
162 161 elrab 
 |-  ( x e. { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } <-> ( x e. ( 1 ... N ) /\ ( k e. Prime /\ k || x ) ) )
163 162 simprbi 
 |-  ( x e. { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } -> ( k e. Prime /\ k || x ) )
164 159 163 syl6bi 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> ( x e. ( W ` k ) -> ( k e. Prime /\ k || x ) ) )
165 156 164 mtod 
 |-  ( ( ( ph /\ x e. M ) /\ k e. ( ( K + 1 ) ... N ) ) -> -. x e. ( W ` k ) )
166 165 nrexdv 
 |-  ( ( ph /\ x e. M ) -> -. E. k e. ( ( K + 1 ) ... N ) x e. ( W ` k ) )
167 eliun 
 |-  ( x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) <-> E. k e. ( ( K + 1 ) ... N ) x e. ( W ` k ) )
168 166 167 sylnibr 
 |-  ( ( ph /\ x e. M ) -> -. x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) )
169 168 ex 
 |-  ( ph -> ( x e. M -> -. x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
170 imnan 
 |-  ( ( x e. M -> -. x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <-> -. ( x e. M /\ x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
171 169 170 sylib 
 |-  ( ph -> -. ( x e. M /\ x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
172 elin 
 |-  ( x e. ( M i^i U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <-> ( x e. M /\ x e. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
173 171 172 sylnibr 
 |-  ( ph -> -. x e. ( M i^i U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
174 173 eq0rdv 
 |-  ( ph -> ( M i^i U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) = (/) )
175 hashun 
 |-  ( ( M e. Fin /\ U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) e. Fin /\ ( M i^i U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) = (/) ) -> ( # ` ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) = ( ( # ` M ) + ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
176 128 130 174 175 syl3anc 
 |-  ( ph -> ( # ` ( M u. U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) = ( ( # ` M ) + ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
177 28 127 176 3eqtrd 
 |-  ( ph -> ( ( N / 2 ) + ( N / 2 ) ) = ( ( # ` M ) + ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) )
178 hashcl 
 |-  ( U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) e. Fin -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) e. NN0 )
179 130 178 syl 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) e. NN0 )
180 179 nn0red 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) e. RR )
181 fzfid 
 |-  ( ph -> ( ( K + 1 ) ... N ) e. Fin )
182 30 32 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN )
183 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
184 0re 
 |-  0 e. RR
185 ifcl 
 |-  ( ( ( 1 / k ) e. RR /\ 0 e. RR ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
186 183 184 185 sylancl 
 |-  ( k e. NN -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
187 182 186 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
188 31 187 sylan2 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
189 181 188 fsumrecl 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
190 8 189 remulcld 
 |-  ( ph -> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) e. RR )
191 1 2 3 4 5 6 7 prmreclem4 
 |-  ( ph -> ( N e. ( ZZ>= ` K ) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
192 eluz 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( K e. ( ZZ>= ` N ) <-> N <_ K ) )
193 98 70 192 syl2anc 
 |-  ( ph -> ( K e. ( ZZ>= ` N ) <-> N <_ K ) )
194 nnleltp1 
 |-  ( ( N e. NN /\ K e. NN ) -> ( N <_ K <-> N < ( K + 1 ) ) )
195 3 2 194 syl2anc 
 |-  ( ph -> ( N <_ K <-> N < ( K + 1 ) ) )
196 fzn 
 |-  ( ( ( K + 1 ) e. ZZ /\ N e. ZZ ) -> ( N < ( K + 1 ) <-> ( ( K + 1 ) ... N ) = (/) ) )
197 96 98 196 syl2anc 
 |-  ( ph -> ( N < ( K + 1 ) <-> ( ( K + 1 ) ... N ) = (/) ) )
198 193 195 197 3bitrd 
 |-  ( ph -> ( K e. ( ZZ>= ` N ) <-> ( ( K + 1 ) ... N ) = (/) ) )
199 0le0 
 |-  0 <_ 0
200 27 mul01d 
 |-  ( ph -> ( N x. 0 ) = 0 )
201 199 200 breqtrrid 
 |-  ( ph -> 0 <_ ( N x. 0 ) )
202 iuneq1 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) = U_ k e. (/) ( W ` k ) )
203 0iun 
 |-  U_ k e. (/) ( W ` k ) = (/)
204 202 203 eqtrdi 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) = (/) )
205 204 fveq2d 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) = ( # ` (/) ) )
206 hash0 
 |-  ( # ` (/) ) = 0
207 205 206 eqtrdi 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) = 0 )
208 sumeq1 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. (/) if ( k e. Prime , ( 1 / k ) , 0 ) )
209 sum0 
 |-  sum_ k e. (/) if ( k e. Prime , ( 1 / k ) , 0 ) = 0
210 208 209 eqtrdi 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) = 0 )
211 210 oveq2d 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. 0 ) )
212 207 211 breq12d 
 |-  ( ( ( K + 1 ) ... N ) = (/) -> ( ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> 0 <_ ( N x. 0 ) ) )
213 201 212 syl5ibrcom 
 |-  ( ph -> ( ( ( K + 1 ) ... N ) = (/) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
214 198 213 sylbid 
 |-  ( ph -> ( K e. ( ZZ>= ` N ) -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
215 uztric 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` K ) \/ K e. ( ZZ>= ` N ) ) )
216 70 98 215 syl2anc 
 |-  ( ph -> ( N e. ( ZZ>= ` K ) \/ K e. ( ZZ>= ` N ) ) )
217 191 214 216 mpjaod 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
218 eqid 
 |-  ( ZZ>= ` ( K + 1 ) ) = ( ZZ>= ` ( K + 1 ) )
219 eleq1w 
 |-  ( n = k -> ( n e. Prime <-> k e. Prime ) )
220 oveq2 
 |-  ( n = k -> ( 1 / n ) = ( 1 / k ) )
221 219 220 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( 1 / n ) , 0 ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
222 ovex 
 |-  ( 1 / k ) e. _V
223 c0ex 
 |-  0 e. _V
224 222 223 ifex 
 |-  if ( k e. Prime , ( 1 / k ) , 0 ) e. _V
225 221 1 224 fvmpt 
 |-  ( k e. NN -> ( F ` k ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
226 182 225 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> ( F ` k ) = if ( k e. Prime , ( 1 / k ) , 0 ) )
227 186 recnd 
 |-  ( k e. NN -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
228 225 227 eqeltrd 
 |-  ( k e. NN -> ( F ` k ) e. CC )
229 228 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
230 68 30 229 iserex 
 |-  ( ph -> ( seq 1 ( + , F ) e. dom ~~> <-> seq ( K + 1 ) ( + , F ) e. dom ~~> ) )
231 5 230 mpbid 
 |-  ( ph -> seq ( K + 1 ) ( + , F ) e. dom ~~> )
232 218 96 226 187 231 isumrecl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
233 halfre 
 |-  ( 1 / 2 ) e. RR
234 233 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
235 fzssuz 
 |-  ( ( K + 1 ) ... N ) C_ ( ZZ>= ` ( K + 1 ) )
236 235 a1i 
 |-  ( ph -> ( ( K + 1 ) ... N ) C_ ( ZZ>= ` ( K + 1 ) ) )
237 nnrp 
 |-  ( k e. NN -> k e. RR+ )
238 237 rpreccld 
 |-  ( k e. NN -> ( 1 / k ) e. RR+ )
239 238 rpge0d 
 |-  ( k e. NN -> 0 <_ ( 1 / k ) )
240 breq2 
 |-  ( ( 1 / k ) = if ( k e. Prime , ( 1 / k ) , 0 ) -> ( 0 <_ ( 1 / k ) <-> 0 <_ if ( k e. Prime , ( 1 / k ) , 0 ) ) )
241 breq2 
 |-  ( 0 = if ( k e. Prime , ( 1 / k ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( k e. Prime , ( 1 / k ) , 0 ) ) )
242 240 241 ifboth 
 |-  ( ( 0 <_ ( 1 / k ) /\ 0 <_ 0 ) -> 0 <_ if ( k e. Prime , ( 1 / k ) , 0 ) )
243 239 199 242 sylancl 
 |-  ( k e. NN -> 0 <_ if ( k e. Prime , ( 1 / k ) , 0 ) )
244 182 243 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> 0 <_ if ( k e. Prime , ( 1 / k ) , 0 ) )
245 218 96 181 236 226 187 244 231 isumless 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) <_ sum_ k e. ( ZZ>= ` ( K + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) )
246 189 232 234 245 6 lelttrd 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) )
247 3 nngt0d 
 |-  ( ph -> 0 < N )
248 ltmul2 
 |-  ( ( sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) e. RR /\ ( 1 / 2 ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) <-> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) < ( N x. ( 1 / 2 ) ) ) )
249 189 234 8 247 248 syl112anc 
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) < ( 1 / 2 ) <-> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) < ( N x. ( 1 / 2 ) ) ) )
250 246 249 mpbid 
 |-  ( ph -> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) < ( N x. ( 1 / 2 ) ) )
251 2cn 
 |-  2 e. CC
252 2ne0 
 |-  2 =/= 0
253 divrec 
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( N / 2 ) = ( N x. ( 1 / 2 ) ) )
254 251 252 253 mp3an23 
 |-  ( N e. CC -> ( N / 2 ) = ( N x. ( 1 / 2 ) ) )
255 27 254 syl 
 |-  ( ph -> ( N / 2 ) = ( N x. ( 1 / 2 ) ) )
256 250 255 breqtrrd 
 |-  ( ph -> ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) < ( N / 2 ) )
257 180 190 9 217 256 lelttrd 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) < ( N / 2 ) )
258 180 9 17 257 ltadd2dd 
 |-  ( ph -> ( ( # ` M ) + ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) ) < ( ( # ` M ) + ( N / 2 ) ) )
259 177 258 eqbrtrd 
 |-  ( ph -> ( ( N / 2 ) + ( N / 2 ) ) < ( ( # ` M ) + ( N / 2 ) ) )
260 9 17 9 ltadd1d 
 |-  ( ph -> ( ( N / 2 ) < ( # ` M ) <-> ( ( N / 2 ) + ( N / 2 ) ) < ( ( # ` M ) + ( N / 2 ) ) ) )
261 259 260 mpbird 
 |-  ( ph -> ( N / 2 ) < ( # ` M ) )
262 oveq1 
 |-  ( k = r -> ( k ^ 2 ) = ( r ^ 2 ) )
263 262 breq1d 
 |-  ( k = r -> ( ( k ^ 2 ) || x <-> ( r ^ 2 ) || x ) )
264 263 cbvrabv 
 |-  { k e. NN | ( k ^ 2 ) || x } = { r e. NN | ( r ^ 2 ) || x }
265 breq2 
 |-  ( x = n -> ( ( r ^ 2 ) || x <-> ( r ^ 2 ) || n ) )
266 265 rabbidv 
 |-  ( x = n -> { r e. NN | ( r ^ 2 ) || x } = { r e. NN | ( r ^ 2 ) || n } )
267 264 266 syl5eq 
 |-  ( x = n -> { k e. NN | ( k ^ 2 ) || x } = { r e. NN | ( r ^ 2 ) || n } )
268 267 supeq1d 
 |-  ( x = n -> sup ( { k e. NN | ( k ^ 2 ) || x } , RR , < ) = sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
269 268 cbvmptv 
 |-  ( x e. NN |-> sup ( { k e. NN | ( k ^ 2 ) || x } , RR , < ) ) = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
270 1 2 3 4 269 prmreclem3 
 |-  ( ph -> ( # ` M ) <_ ( ( 2 ^ K ) x. ( sqrt ` N ) ) )
271 9 17 26 261 270 ltletrd 
 |-  ( ph -> ( N / 2 ) < ( ( 2 ^ K ) x. ( sqrt ` N ) ) )