Metamath Proof Explorer

Theorem prmreclem4

Description: Lemma for prmrec . Show by induction that the indexed (nondisjoint) union Wk is at most the size of the prime reciprocal series. The key counting lemma is hashdvds , to show that the number of numbers in 1 ... N that divide k is at most N / k . (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 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 ) ) ) )

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 oveq2 
 |-  ( x = K -> ( ( K + 1 ) ... x ) = ( ( K + 1 ) ... K ) )
9 8 iuneq1d 
 |-  ( x = K -> U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) = U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) )
10 9 fveq2d 
 |-  ( x = K -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) = ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) )
11 8 sumeq1d 
 |-  ( x = K -> sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) )
12 11 oveq2d 
 |-  ( x = K -> ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
13 10 12 breq12d 
 |-  ( x = K -> ( ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
14 13 imbi2d 
 |-  ( x = K -> ( ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) <-> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
15 oveq2 
 |-  ( x = j -> ( ( K + 1 ) ... x ) = ( ( K + 1 ) ... j ) )
16 15 iuneq1d 
 |-  ( x = j -> U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) = U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) )
17 16 fveq2d 
 |-  ( x = j -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) = ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) )
18 15 sumeq1d 
 |-  ( x = j -> sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) )
19 18 oveq2d 
 |-  ( x = j -> ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
20 17 19 breq12d 
 |-  ( x = j -> ( ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
21 20 imbi2d 
 |-  ( x = j -> ( ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) <-> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
22 oveq2 
 |-  ( x = ( j + 1 ) -> ( ( K + 1 ) ... x ) = ( ( K + 1 ) ... ( j + 1 ) ) )
23 22 iuneq1d 
 |-  ( x = ( j + 1 ) -> U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) = U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) )
24 23 fveq2d 
 |-  ( x = ( j + 1 ) -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) = ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) )
25 22 sumeq1d 
 |-  ( x = ( j + 1 ) -> sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) )
26 25 oveq2d 
 |-  ( x = ( j + 1 ) -> ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
27 24 26 breq12d 
 |-  ( x = ( j + 1 ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
28 27 imbi2d 
 |-  ( x = ( j + 1 ) -> ( ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) <-> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
29 oveq2 
 |-  ( x = N -> ( ( K + 1 ) ... x ) = ( ( K + 1 ) ... N ) )
30 29 iuneq1d 
 |-  ( x = N -> U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) = U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) )
31 30 fveq2d 
 |-  ( x = N -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) = ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) )
32 29 sumeq1d 
 |-  ( x = N -> sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) )
33 32 oveq2d 
 |-  ( x = N -> ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
34 31 33 breq12d 
 |-  ( x = N -> ( ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
35 34 imbi2d 
 |-  ( x = N -> ( ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... x ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... x ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) <-> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
36 0le0 
 |-  0 <_ 0
37 3 nncnd 
 |-  ( ph -> N e. CC )
38 37 mul01d 
 |-  ( ph -> ( N x. 0 ) = 0 )
39 36 38 breqtrrid 
 |-  ( ph -> 0 <_ ( N x. 0 ) )
40 2 nnred 
 |-  ( ph -> K e. RR )
41 40 ltp1d 
 |-  ( ph -> K < ( K + 1 ) )
42 2 nnzd 
 |-  ( ph -> K e. ZZ )
43 42 peano2zd 
 |-  ( ph -> ( K + 1 ) e. ZZ )
44 fzn 
 |-  ( ( ( K + 1 ) e. ZZ /\ K e. ZZ ) -> ( K < ( K + 1 ) <-> ( ( K + 1 ) ... K ) = (/) ) )
45 43 42 44 syl2anc 
 |-  ( ph -> ( K < ( K + 1 ) <-> ( ( K + 1 ) ... K ) = (/) ) )
46 41 45 mpbid 
 |-  ( ph -> ( ( K + 1 ) ... K ) = (/) )
47 46 iuneq1d 
 |-  ( ph -> U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) = U_ k e. (/) ( W ` k ) )
48 0iun 
 |-  U_ k e. (/) ( W ` k ) = (/)
49 47 48 eqtrdi 
 |-  ( ph -> U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) = (/) )
50 49 fveq2d 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) = ( # ` (/) ) )
51 hash0 
 |-  ( # ` (/) ) = 0
52 50 51 eqtrdi 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) = 0 )
53 46 sumeq1d 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. (/) if ( k e. Prime , ( 1 / k ) , 0 ) )
54 sum0 
 |-  sum_ k e. (/) if ( k e. Prime , ( 1 / k ) , 0 ) = 0
55 53 54 eqtrdi 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) = 0 )
56 55 oveq2d 
 |-  ( ph -> ( N x. sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. 0 ) )
57 39 52 56 3brtr4d 
 |-  ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... K ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... K ) if ( k e. Prime , ( 1 / k ) , 0 ) ) )
58 fzfi 
 |-  ( 1 ... N ) e. Fin
59 elfzuz 
 |-  ( k e. ( ( K + 1 ) ... j ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
60 2 peano2nnd 
 |-  ( ph -> ( K + 1 ) e. NN )
61 eluznn 
 |-  ( ( ( K + 1 ) e. NN /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN )
62 60 61 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN )
63 eleq1 
 |-  ( p = k -> ( p e. Prime <-> k e. Prime ) )
64 breq1 
 |-  ( p = k -> ( p || n <-> k || n ) )
65 63 64 anbi12d 
 |-  ( p = k -> ( ( p e. Prime /\ p || n ) <-> ( k e. Prime /\ k || n ) ) )
66 65 rabbidv 
 |-  ( p = k -> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
67 ovex 
 |-  ( 1 ... N ) e. _V
68 67 rabex 
 |-  { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } e. _V
69 66 7 68 fvmpt 
 |-  ( k e. NN -> ( W ` k ) = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
70 69 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( W ` k ) = { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } )
71 ssrab2 
 |-  { n e. ( 1 ... N ) | ( k e. Prime /\ k || n ) } C_ ( 1 ... N )
72 70 71 eqsstrdi 
 |-  ( ( ph /\ k e. NN ) -> ( W ` k ) C_ ( 1 ... N ) )
73 62 72 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> ( W ` k ) C_ ( 1 ... N ) )
74 59 73 sylan2 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... j ) ) -> ( W ` k ) C_ ( 1 ... N ) )
75 74 ralrimiva 
 |-  ( ph -> A. k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) )
76 75 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> A. k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) )
77 iunss 
 |-  ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) <-> A. k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) )
78 76 77 sylibr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) )
79 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) C_ ( 1 ... N ) ) -> U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) e. Fin )
80 58 78 79 sylancr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) e. Fin )
81 hashcl 
 |-  ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) e. Fin -> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) e. NN0 )
82 80 81 syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) e. NN0 )
83 82 nn0red 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) e. RR )
84 3 nnred 
 |-  ( ph -> N e. RR )
85 84 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> N e. RR )
86 fzfid 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) ... j ) e. Fin )
87 60 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. NN )
88 87 59 61 syl2an 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ k e. ( ( K + 1 ) ... j ) ) -> k e. NN )
89 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
90 0re 
 |-  0 e. RR
91 ifcl 
 |-  ( ( ( 1 / k ) e. RR /\ 0 e. RR ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
92 89 90 91 sylancl 
 |-  ( k e. NN -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
93 88 92 syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ k e. ( ( K + 1 ) ... j ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
94 86 93 fsumrecl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
95 85 94 remulcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) e. RR )
96 prmnn 
 |-  ( ( j + 1 ) e. Prime -> ( j + 1 ) e. NN )
97 96 nnrecred 
 |-  ( ( j + 1 ) e. Prime -> ( 1 / ( j + 1 ) ) e. RR )
98 97 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( 1 / ( j + 1 ) ) e. RR )
99 0red 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> 0 e. RR )
100 98 99 ifclda 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) e. RR )
101 85 100 remulcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) e. RR )
102 83 95 101 leadd1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) ) )
103 eluzp1p1 
 |-  ( j e. ( ZZ>= ` K ) -> ( j + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
104 103 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
105 simpl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ph )
106 elfzuz 
 |-  ( k e. ( ( K + 1 ) ... ( j + 1 ) ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
107 92 recnd 
 |-  ( k e. NN -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
108 62 107 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
109 105 106 108 syl2an 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ k e. ( ( K + 1 ) ... ( j + 1 ) ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
110 eleq1 
 |-  ( k = ( j + 1 ) -> ( k e. Prime <-> ( j + 1 ) e. Prime ) )
111 oveq2 
 |-  ( k = ( j + 1 ) -> ( 1 / k ) = ( 1 / ( j + 1 ) ) )
112 110 111 ifbieq1d 
 |-  ( k = ( j + 1 ) -> if ( k e. Prime , ( 1 / k ) , 0 ) = if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) )
113 104 109 112 fsumm1 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) = ( sum_ k e. ( ( K + 1 ) ... ( ( j + 1 ) - 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
114 eluzelz 
 |-  ( j e. ( ZZ>= ` K ) -> j e. ZZ )
115 114 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ZZ )
116 115 zcnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. CC )
117 ax-1cn 
 |-  1 e. CC
118 pncan 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j + 1 ) - 1 ) = j )
119 116 117 118 sylancl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( j + 1 ) - 1 ) = j )
120 119 oveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) ... ( ( j + 1 ) - 1 ) ) = ( ( K + 1 ) ... j ) )
121 120 sumeq1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... ( ( j + 1 ) - 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) = sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) )
122 121 oveq1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( sum_ k e. ( ( K + 1 ) ... ( ( j + 1 ) - 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) = ( sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
123 113 122 eqtrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) = ( sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
124 123 oveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( N x. ( sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) )
125 37 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> N e. CC )
126 94 recnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) e. CC )
127 100 recnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) e. CC )
128 125 126 127 adddid 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. ( sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) + if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) = ( ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) )
129 124 128 eqtrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) = ( ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) )
130 129 breq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) ) )
131 102 130 bitr4d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) <-> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
132 106 73 sylan2 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... ( j + 1 ) ) ) -> ( W ` k ) C_ ( 1 ... N ) )
133 132 ralrimiva 
 |-  ( ph -> A. k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) )
134 133 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> A. k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) )
135 iunss 
 |-  ( U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) <-> A. k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) )
136 134 135 sylibr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) )
137 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) C_ ( 1 ... N ) ) -> U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) e. Fin )
138 58 136 137 sylancr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) e. Fin )
139 hashcl 
 |-  ( U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) e. Fin -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) e. NN0 )
140 138 139 syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) e. NN0 )
141 140 nn0red 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) e. RR )
142 fveq2 
 |-  ( k = ( j + 1 ) -> ( W ` k ) = ( W ` ( j + 1 ) ) )
143 142 sseq1d 
 |-  ( k = ( j + 1 ) -> ( ( W ` k ) C_ ( 1 ... N ) <-> ( W ` ( j + 1 ) ) C_ ( 1 ... N ) ) )
144 72 ralrimiva 
 |-  ( ph -> A. k e. NN ( W ` k ) C_ ( 1 ... N ) )
145 144 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> A. k e. NN ( W ` k ) C_ ( 1 ... N ) )
146 eluznn 
 |-  ( ( K e. NN /\ j e. ( ZZ>= ` K ) ) -> j e. NN )
147 2 146 sylan 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. NN )
148 147 peano2nnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j + 1 ) e. NN )
149 143 145 148 rspcdva 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( W ` ( j + 1 ) ) C_ ( 1 ... N ) )
150 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( W ` ( j + 1 ) ) C_ ( 1 ... N ) ) -> ( W ` ( j + 1 ) ) e. Fin )
151 58 149 150 sylancr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( W ` ( j + 1 ) ) e. Fin )
152 hashcl 
 |-  ( ( W ` ( j + 1 ) ) e. Fin -> ( # ` ( W ` ( j + 1 ) ) ) e. NN0 )
153 151 152 syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` ( W ` ( j + 1 ) ) ) e. NN0 )
154 153 nn0red 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` ( W ` ( j + 1 ) ) ) e. RR )
155 83 154 readdcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( # ` ( W ` ( j + 1 ) ) ) ) e. RR )
156 83 101 readdcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) e. RR )
157 43 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( K + 1 ) e. ZZ )
158 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ( ZZ>= ` K ) )
159 2 nncnd 
 |-  ( ph -> K e. CC )
160 159 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> K e. CC )
161 pncan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K + 1 ) - 1 ) = K )
162 160 117 161 sylancl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) - 1 ) = K )
163 162 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` ( ( K + 1 ) - 1 ) ) = ( ZZ>= ` K ) )
164 158 163 eleqtrrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ( ZZ>= ` ( ( K + 1 ) - 1 ) ) )
165 fzsuc2 
 |-  ( ( ( K + 1 ) e. ZZ /\ j e. ( ZZ>= ` ( ( K + 1 ) - 1 ) ) ) -> ( ( K + 1 ) ... ( j + 1 ) ) = ( ( ( K + 1 ) ... j ) u. { ( j + 1 ) } ) )
166 157 164 165 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) ... ( j + 1 ) ) = ( ( ( K + 1 ) ... j ) u. { ( j + 1 ) } ) )
167 166 iuneq1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) = U_ k e. ( ( ( K + 1 ) ... j ) u. { ( j + 1 ) } ) ( W ` k ) )
168 iunxun 
 |-  U_ k e. ( ( ( K + 1 ) ... j ) u. { ( j + 1 ) } ) ( W ` k ) = ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. U_ k e. { ( j + 1 ) } ( W ` k ) )
169 ovex 
 |-  ( j + 1 ) e. _V
170 169 142 iunxsn 
 |-  U_ k e. { ( j + 1 ) } ( W ` k ) = ( W ` ( j + 1 ) )
171 170 uneq2i 
 |-  ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. U_ k e. { ( j + 1 ) } ( W ` k ) ) = ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) )
172 168 171 eqtri 
 |-  U_ k e. ( ( ( K + 1 ) ... j ) u. { ( j + 1 ) } ) ( W ` k ) = ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) )
173 167 172 eqtrdi 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) = ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) ) )
174 173 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) = ( # ` ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) ) ) )
175 hashun2 
 |-  ( ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) e. Fin /\ ( W ` ( j + 1 ) ) e. Fin ) -> ( # ` ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( # ` ( W ` ( j + 1 ) ) ) ) )
176 80 151 175 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` ( U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) u. ( W ` ( j + 1 ) ) ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( # ` ( W ` ( j + 1 ) ) ) ) )
177 174 176 eqbrtrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( # ` ( W ` ( j + 1 ) ) ) ) )
178 85 148 nndivred 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N / ( j + 1 ) ) e. RR )
179 flle 
 |-  ( ( N / ( j + 1 ) ) e. RR -> ( |_ ` ( N / ( j + 1 ) ) ) <_ ( N / ( j + 1 ) ) )
180 178 179 syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( N / ( j + 1 ) ) ) <_ ( N / ( j + 1 ) ) )
181 elfznn 
 |-  ( n e. ( 1 ... N ) -> n e. NN )
182 181 nncnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
183 182 subid1d 
 |-  ( n e. ( 1 ... N ) -> ( n - 0 ) = n )
184 183 breq2d 
 |-  ( n e. ( 1 ... N ) -> ( ( j + 1 ) || ( n - 0 ) <-> ( j + 1 ) || n ) )
185 184 rabbiia 
 |-  { n e. ( 1 ... N ) | ( j + 1 ) || ( n - 0 ) } = { n e. ( 1 ... N ) | ( j + 1 ) || n }
186 185 fveq2i 
 |-  ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || ( n - 0 ) } ) = ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || n } )
187 1zzd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> 1 e. ZZ )
188 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
189 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
190 1m1e0 
 |-  ( 1 - 1 ) = 0
191 190 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
192 189 191 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
193 188 192 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
194 193 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
195 0zd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> 0 e. ZZ )
196 148 187 194 195 hashdvds 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || ( n - 0 ) } ) = ( ( |_ ` ( ( N - 0 ) / ( j + 1 ) ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) ) ) )
197 125 subid1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N - 0 ) = N )
198 197 fvoveq1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( ( N - 0 ) / ( j + 1 ) ) ) = ( |_ ` ( N / ( j + 1 ) ) ) )
199 190 oveq1i 
 |-  ( ( 1 - 1 ) - 0 ) = ( 0 - 0 )
200 0m0e0 
 |-  ( 0 - 0 ) = 0
201 199 200 eqtri 
 |-  ( ( 1 - 1 ) - 0 ) = 0
202 201 oveq1i 
 |-  ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) = ( 0 / ( j + 1 ) )
203 148 nncnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j + 1 ) e. CC )
204 148 nnne0d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j + 1 ) =/= 0 )
205 203 204 div0d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( 0 / ( j + 1 ) ) = 0 )
206 202 205 syl5eq 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) = 0 )
207 206 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) ) = ( |_ ` 0 ) )
208 0z 
 |-  0 e. ZZ
209 flid 
 |-  ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
210 208 209 ax-mp 
 |-  ( |_ ` 0 ) = 0
211 207 210 eqtrdi 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) ) = 0 )
212 198 211 oveq12d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( |_ ` ( ( N - 0 ) / ( j + 1 ) ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / ( j + 1 ) ) ) ) = ( ( |_ ` ( N / ( j + 1 ) ) ) - 0 ) )
213 178 flcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( N / ( j + 1 ) ) ) e. ZZ )
214 213 zcnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( |_ ` ( N / ( j + 1 ) ) ) e. CC )
215 214 subid1d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( |_ ` ( N / ( j + 1 ) ) ) - 0 ) = ( |_ ` ( N / ( j + 1 ) ) ) )
216 196 212 215 3eqtrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || ( n - 0 ) } ) = ( |_ ` ( N / ( j + 1 ) ) ) )
217 186 216 syl5eqr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || n } ) = ( |_ ` ( N / ( j + 1 ) ) ) )
218 125 203 204 divrecd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N / ( j + 1 ) ) = ( N x. ( 1 / ( j + 1 ) ) ) )
219 218 eqcomd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. ( 1 / ( j + 1 ) ) ) = ( N / ( j + 1 ) ) )
220 180 217 219 3brtr4d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || n } ) <_ ( N x. ( 1 / ( j + 1 ) ) ) )
221 220 adantr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || n } ) <_ ( N x. ( 1 / ( j + 1 ) ) ) )
222 eleq1 
 |-  ( p = ( j + 1 ) -> ( p e. Prime <-> ( j + 1 ) e. Prime ) )
223 breq1 
 |-  ( p = ( j + 1 ) -> ( p || n <-> ( j + 1 ) || n ) )
224 222 223 anbi12d 
 |-  ( p = ( j + 1 ) -> ( ( p e. Prime /\ p || n ) <-> ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) ) )
225 224 rabbidv 
 |-  ( p = ( j + 1 ) -> { n e. ( 1 ... N ) | ( p e. Prime /\ p || n ) } = { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } )
226 67 rabex 
 |-  { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } e. _V
227 225 7 226 fvmpt 
 |-  ( ( j + 1 ) e. NN -> ( W ` ( j + 1 ) ) = { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } )
228 148 227 syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( W ` ( j + 1 ) ) = { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } )
229 228 adantr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( W ` ( j + 1 ) ) = { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } )
230 simpr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( j + 1 ) e. Prime )
231 230 biantrurd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( ( j + 1 ) || n <-> ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) ) )
232 231 rabbidv 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> { n e. ( 1 ... N ) | ( j + 1 ) || n } = { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } )
233 229 232 eqtr4d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( W ` ( j + 1 ) ) = { n e. ( 1 ... N ) | ( j + 1 ) || n } )
234 233 fveq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( # ` ( W ` ( j + 1 ) ) ) = ( # ` { n e. ( 1 ... N ) | ( j + 1 ) || n } ) )
235 iftrue 
 |-  ( ( j + 1 ) e. Prime -> if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) = ( 1 / ( j + 1 ) ) )
236 235 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) = ( 1 / ( j + 1 ) ) )
237 236 oveq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) = ( N x. ( 1 / ( j + 1 ) ) ) )
238 221 234 237 3brtr4d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ ( j + 1 ) e. Prime ) -> ( # ` ( W ` ( j + 1 ) ) ) <_ ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
239 36 a1i 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> 0 <_ 0 )
240 simpl 
 |-  ( ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) -> ( j + 1 ) e. Prime )
241 240 con3i 
 |-  ( -. ( j + 1 ) e. Prime -> -. ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) )
242 241 ralrimivw 
 |-  ( -. ( j + 1 ) e. Prime -> A. n e. ( 1 ... N ) -. ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) )
243 rabeq0 
 |-  ( { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } = (/) <-> A. n e. ( 1 ... N ) -. ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) )
244 242 243 sylibr 
 |-  ( -. ( j + 1 ) e. Prime -> { n e. ( 1 ... N ) | ( ( j + 1 ) e. Prime /\ ( j + 1 ) || n ) } = (/) )
245 228 244 sylan9eq 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> ( W ` ( j + 1 ) ) = (/) )
246 245 fveq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> ( # ` ( W ` ( j + 1 ) ) ) = ( # ` (/) ) )
247 246 51 eqtrdi 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> ( # ` ( W ` ( j + 1 ) ) ) = 0 )
248 iffalse 
 |-  ( -. ( j + 1 ) e. Prime -> if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) = 0 )
249 248 oveq2d 
 |-  ( -. ( j + 1 ) e. Prime -> ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) = ( N x. 0 ) )
250 38 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. 0 ) = 0 )
251 249 250 sylan9eqr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) = 0 )
252 239 247 251 3brtr4d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ -. ( j + 1 ) e. Prime ) -> ( # ` ( W ` ( j + 1 ) ) ) <_ ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
253 238 252 pm2.61dan 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` ( W ` ( j + 1 ) ) ) <_ ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) )
254 154 101 83 253 leadd2dd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( # ` ( W ` ( j + 1 ) ) ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) )
255 141 155 156 177 254 letrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) )
256 fzfid 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) ... ( j + 1 ) ) e. Fin )
257 62 92 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
258 105 106 257 syl2an 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` K ) ) /\ k e. ( ( K + 1 ) ... ( j + 1 ) ) ) -> if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
259 256 258 fsumrecl 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) e. RR )
260 85 259 remulcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) e. RR )
261 letr 
 |-  ( ( ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) e. RR /\ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) e. RR /\ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) e. RR ) -> ( ( ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) /\ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
262 141 156 260 261 syl3anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) /\ ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
263 255 262 mpand 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) + ( N x. if ( ( j + 1 ) e. Prime , ( 1 / ( j + 1 ) ) , 0 ) ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
264 131 263 sylbid 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
265 264 expcom 
 |-  ( j e. ( ZZ>= ` K ) -> ( ph -> ( ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
266 265 a2d 
 |-  ( j e. ( ZZ>= ` K ) -> ( ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... j ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... j ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) -> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... ( j + 1 ) ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... ( j + 1 ) ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) ) )
267 14 21 28 35 57 266 uzind4i 
 |-  ( N e. ( ZZ>= ` K ) -> ( ph -> ( # ` U_ k e. ( ( K + 1 ) ... N ) ( W ` k ) ) <_ ( N x. sum_ k e. ( ( K + 1 ) ... N ) if ( k e. Prime , ( 1 / k ) , 0 ) ) ) )
268 267 com12 
 |-  ( 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 ) ) ) )