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 ) ) ) ) |