Step |
Hyp |
Ref |
Expression |
1 |
|
pntlem1.r |
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) ) |
2 |
|
pntlem1.a |
|- ( ph -> A e. RR+ ) |
3 |
|
pntlem1.b |
|- ( ph -> B e. RR+ ) |
4 |
|
pntlem1.l |
|- ( ph -> L e. ( 0 (,) 1 ) ) |
5 |
|
pntlem1.d |
|- D = ( A + 1 ) |
6 |
|
pntlem1.f |
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) |
7 |
|
pntlem1.u |
|- ( ph -> U e. RR+ ) |
8 |
|
pntlem1.u2 |
|- ( ph -> U <_ A ) |
9 |
|
pntlem1.e |
|- E = ( U / D ) |
10 |
|
pntlem1.k |
|- K = ( exp ` ( B / E ) ) |
11 |
|
pntlem1.y |
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) ) |
12 |
|
pntlem1.x |
|- ( ph -> ( X e. RR+ /\ Y < X ) ) |
13 |
|
pntlem1.c |
|- ( ph -> C e. RR+ ) |
14 |
|
pntlem1.w |
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) |
15 |
|
pntlem1.z |
|- ( ph -> Z e. ( W [,) +oo ) ) |
16 |
|
pntlem1.m |
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) |
17 |
|
pntlem1.n |
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) |
18 |
|
pntlem1.U |
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U ) |
19 |
|
pntlem1.K |
|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) |
20 |
|
2re |
|- 2 e. RR |
21 |
|
fzfid |
|- ( ph -> ( 1 ... ( |_ ` ( Z / Y ) ) ) e. Fin ) |
22 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n e. NN ) |
23 |
22
|
adantl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. NN ) |
24 |
23
|
nnrpd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. RR+ ) |
25 |
24
|
relogcld |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. RR ) |
26 |
25 23
|
nndivred |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. RR ) |
27 |
21 26
|
fsumrecl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR ) |
28 |
|
remulcl |
|- ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR ) |
29 |
20 27 28
|
sylancr |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR ) |
30 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
pntlemb |
|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) ) |
31 |
30
|
simp1d |
|- ( ph -> Z e. RR+ ) |
32 |
31
|
relogcld |
|- ( ph -> ( log ` Z ) e. RR ) |
33 |
|
peano2re |
|- ( ( log ` Z ) e. RR -> ( ( log ` Z ) + 1 ) e. RR ) |
34 |
32 33
|
syl |
|- ( ph -> ( ( log ` Z ) + 1 ) e. RR ) |
35 |
34
|
resqcld |
|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) e. RR ) |
36 |
|
3re |
|- 3 e. RR |
37 |
|
readdcl |
|- ( ( ( log ` Z ) e. RR /\ 3 e. RR ) -> ( ( log ` Z ) + 3 ) e. RR ) |
38 |
32 36 37
|
sylancl |
|- ( ph -> ( ( log ` Z ) + 3 ) e. RR ) |
39 |
38 32
|
remulcld |
|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) e. RR ) |
40 |
31
|
rpred |
|- ( ph -> Z e. RR ) |
41 |
11
|
simpld |
|- ( ph -> Y e. RR+ ) |
42 |
40 41
|
rerpdivcld |
|- ( ph -> ( Z / Y ) e. RR ) |
43 |
|
1red |
|- ( ph -> 1 e. RR ) |
44 |
31
|
rpsqrtcld |
|- ( ph -> ( sqrt ` Z ) e. RR+ ) |
45 |
44
|
rpred |
|- ( ph -> ( sqrt ` Z ) e. RR ) |
46 |
|
ere |
|- _e e. RR |
47 |
46
|
a1i |
|- ( ph -> _e e. RR ) |
48 |
|
1re |
|- 1 e. RR |
49 |
|
1lt2 |
|- 1 < 2 |
50 |
|
egt2lt3 |
|- ( 2 < _e /\ _e < 3 ) |
51 |
50
|
simpli |
|- 2 < _e |
52 |
48 20 46
|
lttri |
|- ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e ) |
53 |
49 51 52
|
mp2an |
|- 1 < _e |
54 |
48 46 53
|
ltleii |
|- 1 <_ _e |
55 |
54
|
a1i |
|- ( ph -> 1 <_ _e ) |
56 |
30
|
simp2d |
|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) ) |
57 |
56
|
simp2d |
|- ( ph -> _e <_ ( sqrt ` Z ) ) |
58 |
43 47 45 55 57
|
letrd |
|- ( ph -> 1 <_ ( sqrt ` Z ) ) |
59 |
56
|
simp3d |
|- ( ph -> ( sqrt ` Z ) <_ ( Z / Y ) ) |
60 |
43 45 42 58 59
|
letrd |
|- ( ph -> 1 <_ ( Z / Y ) ) |
61 |
|
flge1nn |
|- ( ( ( Z / Y ) e. RR /\ 1 <_ ( Z / Y ) ) -> ( |_ ` ( Z / Y ) ) e. NN ) |
62 |
42 60 61
|
syl2anc |
|- ( ph -> ( |_ ` ( Z / Y ) ) e. NN ) |
63 |
62
|
nnrpd |
|- ( ph -> ( |_ ` ( Z / Y ) ) e. RR+ ) |
64 |
63
|
relogcld |
|- ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) e. RR ) |
65 |
64 43
|
readdcld |
|- ( ph -> ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) e. RR ) |
66 |
65
|
resqcld |
|- ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR ) |
67 |
|
logdivbnd |
|- ( ( |_ ` ( Z / Y ) ) e. NN -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) |
68 |
62 67
|
syl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) |
69 |
20
|
a1i |
|- ( ph -> 2 e. RR ) |
70 |
|
2pos |
|- 0 < 2 |
71 |
70
|
a1i |
|- ( ph -> 0 < 2 ) |
72 |
|
lemuldiv2 |
|- ( ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR /\ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) ) |
73 |
27 66 69 71 72
|
syl112anc |
|- ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) ) |
74 |
68 73
|
mpbird |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) ) |
75 |
|
reflcl |
|- ( ( Z / Y ) e. RR -> ( |_ ` ( Z / Y ) ) e. RR ) |
76 |
42 75
|
syl |
|- ( ph -> ( |_ ` ( Z / Y ) ) e. RR ) |
77 |
|
flle |
|- ( ( Z / Y ) e. RR -> ( |_ ` ( Z / Y ) ) <_ ( Z / Y ) ) |
78 |
42 77
|
syl |
|- ( ph -> ( |_ ` ( Z / Y ) ) <_ ( Z / Y ) ) |
79 |
11
|
simprd |
|- ( ph -> 1 <_ Y ) |
80 |
|
1rp |
|- 1 e. RR+ |
81 |
80
|
a1i |
|- ( ph -> 1 e. RR+ ) |
82 |
81 41 31
|
lediv2d |
|- ( ph -> ( 1 <_ Y <-> ( Z / Y ) <_ ( Z / 1 ) ) ) |
83 |
79 82
|
mpbid |
|- ( ph -> ( Z / Y ) <_ ( Z / 1 ) ) |
84 |
40
|
recnd |
|- ( ph -> Z e. CC ) |
85 |
84
|
div1d |
|- ( ph -> ( Z / 1 ) = Z ) |
86 |
83 85
|
breqtrd |
|- ( ph -> ( Z / Y ) <_ Z ) |
87 |
76 42 40 78 86
|
letrd |
|- ( ph -> ( |_ ` ( Z / Y ) ) <_ Z ) |
88 |
63 31
|
logled |
|- ( ph -> ( ( |_ ` ( Z / Y ) ) <_ Z <-> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( log ` Z ) ) ) |
89 |
87 88
|
mpbid |
|- ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( log ` Z ) ) |
90 |
64 32 43 89
|
leadd1dd |
|- ( ph -> ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) ) |
91 |
|
0red |
|- ( ph -> 0 e. RR ) |
92 |
|
log1 |
|- ( log ` 1 ) = 0 |
93 |
62
|
nnge1d |
|- ( ph -> 1 <_ ( |_ ` ( Z / Y ) ) ) |
94 |
|
logleb |
|- ( ( 1 e. RR+ /\ ( |_ ` ( Z / Y ) ) e. RR+ ) -> ( 1 <_ ( |_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) ) |
95 |
80 63 94
|
sylancr |
|- ( ph -> ( 1 <_ ( |_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) ) |
96 |
93 95
|
mpbid |
|- ( ph -> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) |
97 |
92 96
|
eqbrtrrid |
|- ( ph -> 0 <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) |
98 |
64
|
lep1d |
|- ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ) |
99 |
91 64 65 97 98
|
letrd |
|- ( ph -> 0 <_ ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ) |
100 |
91 65 34 99 90
|
letrd |
|- ( ph -> 0 <_ ( ( log ` Z ) + 1 ) ) |
101 |
65 34 99 100
|
le2sqd |
|- ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) <-> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) ) ) |
102 |
90 101
|
mpbid |
|- ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) ) |
103 |
29 66 35 74 102
|
letrd |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) ) |
104 |
32
|
resqcld |
|- ( ph -> ( ( log ` Z ) ^ 2 ) e. RR ) |
105 |
69 32
|
remulcld |
|- ( ph -> ( 2 x. ( log ` Z ) ) e. RR ) |
106 |
104 105
|
readdcld |
|- ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) e. RR ) |
107 |
|
loge |
|- ( log ` _e ) = 1 |
108 |
44
|
rpge0d |
|- ( ph -> 0 <_ ( sqrt ` Z ) ) |
109 |
45 45 108 58
|
lemulge12d |
|- ( ph -> ( sqrt ` Z ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) |
110 |
31
|
rprege0d |
|- ( ph -> ( Z e. RR /\ 0 <_ Z ) ) |
111 |
|
remsqsqrt |
|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
112 |
110 111
|
syl |
|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
113 |
109 112
|
breqtrd |
|- ( ph -> ( sqrt ` Z ) <_ Z ) |
114 |
47 45 40 57 113
|
letrd |
|- ( ph -> _e <_ Z ) |
115 |
|
epr |
|- _e e. RR+ |
116 |
|
logleb |
|- ( ( _e e. RR+ /\ Z e. RR+ ) -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) ) |
117 |
115 31 116
|
sylancr |
|- ( ph -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) ) |
118 |
114 117
|
mpbid |
|- ( ph -> ( log ` _e ) <_ ( log ` Z ) ) |
119 |
107 118
|
eqbrtrrid |
|- ( ph -> 1 <_ ( log ` Z ) ) |
120 |
43 32 106 119
|
leadd2dd |
|- ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) <_ ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) ) |
121 |
32
|
recnd |
|- ( ph -> ( log ` Z ) e. CC ) |
122 |
|
binom21 |
|- ( ( log ` Z ) e. CC -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) ) |
123 |
121 122
|
syl |
|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) ) |
124 |
121
|
sqvald |
|- ( ph -> ( ( log ` Z ) ^ 2 ) = ( ( log ` Z ) x. ( log ` Z ) ) ) |
125 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
126 |
125
|
oveq1i |
|- ( 3 x. ( log ` Z ) ) = ( ( 2 + 1 ) x. ( log ` Z ) ) |
127 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
128 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
129 |
127 128 121
|
adddird |
|- ( ph -> ( ( 2 + 1 ) x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) ) |
130 |
126 129
|
syl5eq |
|- ( ph -> ( 3 x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) ) |
131 |
121
|
mulid2d |
|- ( ph -> ( 1 x. ( log ` Z ) ) = ( log ` Z ) ) |
132 |
131
|
oveq2d |
|- ( ph -> ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) = ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) |
133 |
130 132
|
eqtr2d |
|- ( ph -> ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) = ( 3 x. ( log ` Z ) ) ) |
134 |
124 133
|
oveq12d |
|- ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) ) |
135 |
121
|
sqcld |
|- ( ph -> ( ( log ` Z ) ^ 2 ) e. CC ) |
136 |
|
2cn |
|- 2 e. CC |
137 |
|
mulcl |
|- ( ( 2 e. CC /\ ( log ` Z ) e. CC ) -> ( 2 x. ( log ` Z ) ) e. CC ) |
138 |
136 121 137
|
sylancr |
|- ( ph -> ( 2 x. ( log ` Z ) ) e. CC ) |
139 |
135 138 121
|
addassd |
|- ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) = ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) ) |
140 |
|
3cn |
|- 3 e. CC |
141 |
140
|
a1i |
|- ( ph -> 3 e. CC ) |
142 |
121 141 121
|
adddird |
|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) ) |
143 |
134 139 142
|
3eqtr4rd |
|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) ) |
144 |
120 123 143
|
3brtr4d |
|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) |
145 |
29 35 39 103 144
|
letrd |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) |
146 |
29 39 7
|
lemul2d |
|- ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) <-> ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) ) ) |
147 |
145 146
|
mpbid |
|- ( ph -> ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) ) |
148 |
7
|
rpred |
|- ( ph -> U e. RR ) |
149 |
148
|
adantr |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> U e. RR ) |
150 |
149
|
recnd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> U e. CC ) |
151 |
25
|
recnd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. CC ) |
152 |
24
|
rpcnne0d |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( n e. CC /\ n =/= 0 ) ) |
153 |
|
div23 |
|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( ( U / n ) x. ( log ` n ) ) ) |
154 |
|
divass |
|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( U x. ( ( log ` n ) / n ) ) ) |
155 |
153 154
|
eqtr3d |
|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) ) |
156 |
150 151 152 155
|
syl3anc |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) ) |
157 |
156
|
sumeq2dv |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) ) |
158 |
148
|
recnd |
|- ( ph -> U e. CC ) |
159 |
26
|
recnd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. CC ) |
160 |
21 158 159
|
fsummulc2 |
|- ( ph -> ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) ) |
161 |
157 160
|
eqtr4d |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) |
162 |
161
|
oveq2d |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( 2 x. ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) ) |
163 |
27
|
recnd |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. CC ) |
164 |
127 158 163
|
mul12d |
|- ( ph -> ( 2 x. ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) ) |
165 |
162 164
|
eqtrd |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) ) |
166 |
38
|
recnd |
|- ( ph -> ( ( log ` Z ) + 3 ) e. CC ) |
167 |
158 166 121
|
mulassd |
|- ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) = ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) ) |
168 |
147 165 167
|
3brtr4d |
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) ) |