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