Metamath Proof Explorer

Theorem pntlemo

Description: Lemma for pnt . Combine all the estimates to establish a smaller eventual bound on R ( Z ) / Z . (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem1.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a 
|- ( ph -> A e. RR+ )
pntlem1.b 
|- ( ph -> B e. RR+ )
pntlem1.l 
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d 
|- D = ( A + 1 )
pntlem1.f 
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlem1.u 
|- ( ph -> U e. RR+ )
pntlem1.u2 
|- ( ph -> U <_ A )
pntlem1.e 
|- E = ( U / D )
pntlem1.k 
|- K = ( exp ` ( B / E ) )
pntlem1.y 
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x 
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c 
|- ( ph -> C e. RR+ )
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 ) ) ) ) )
pntlem1.z 
|- ( ph -> Z e. ( W [,) +oo ) )
pntlem1.m 
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
pntlem1.n 
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
pntlem1.U 
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
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 ) )
pntlem1.C 
|- ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )
Assertion pntlemo 
|- ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )

Proof

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 pntlem1.C 
 |-  ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )
21 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 ) ) ) ) )
22 21 simp1d 
 |-  ( ph -> Z e. RR+ )
23 1 pntrf 
 |-  R : RR+ --> RR
24 23 ffvelrni 
 |-  ( Z e. RR+ -> ( R ` Z ) e. RR )
25 22 24 syl 
 |-  ( ph -> ( R ` Z ) e. RR )
26 25 22 rerpdivcld 
 |-  ( ph -> ( ( R ` Z ) / Z ) e. RR )
27 26 recnd 
 |-  ( ph -> ( ( R ` Z ) / Z ) e. CC )
28 27 abscld 
 |-  ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) e. RR )
29 22 relogcld 
 |-  ( ph -> ( log ` Z ) e. RR )
30 28 29 remulcld 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) e. RR )
31 7 rpred 
 |-  ( ph -> U e. RR )
32 3re 
 |-  3 e. RR
33 32 a1i 
 |-  ( ph -> 3 e. RR )
34 29 33 readdcld 
 |-  ( ph -> ( ( log ` Z ) + 3 ) e. RR )
35 31 34 remulcld 
 |-  ( ph -> ( U x. ( ( log ` Z ) + 3 ) ) e. RR )
36 2re 
 |-  2 e. RR
37 36 a1i 
 |-  ( ph -> 2 e. RR )
38 1 2 3 4 5 6 7 8 9 10 pntlemc 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
39 38 simp3d 
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
40 39 simp3d 
 |-  ( ph -> ( U - E ) e. RR+ )
41 40 rpred 
 |-  ( ph -> ( U - E ) e. RR )
42 1 2 3 4 5 6 pntlemd 
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
43 42 simp1d 
 |-  ( ph -> L e. RR+ )
44 38 simp1d 
 |-  ( ph -> E e. RR+ )
45 2z 
 |-  2 e. ZZ
46 rpexpcl 
 |-  ( ( E e. RR+ /\ 2 e. ZZ ) -> ( E ^ 2 ) e. RR+ )
47 44 45 46 sylancl 
 |-  ( ph -> ( E ^ 2 ) e. RR+ )
48 43 47 rpmulcld 
 |-  ( ph -> ( L x. ( E ^ 2 ) ) e. RR+ )
49 3nn0 
 |-  3 e. NN0
50 2nn 
 |-  2 e. NN
51 49 50 decnncl 
 |-  ; 3 2 e. NN
52 nnrp 
 |-  ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
53 51 52 ax-mp 
 |-  ; 3 2 e. RR+
54 rpmulcl 
 |-  ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
55 53 3 54 sylancr 
 |-  ( ph -> ( ; 3 2 x. B ) e. RR+ )
56 48 55 rpdivcld 
 |-  ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) e. RR+ )
57 56 rpred 
 |-  ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) e. RR )
58 41 57 remulcld 
 |-  ( ph -> ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) e. RR )
59 58 29 remulcld 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) e. RR )
60 37 59 remulcld 
 |-  ( ph -> ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) e. RR )
61 35 60 resubcld 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) e. RR )
62 13 rpred 
 |-  ( ph -> C e. RR )
63 61 62 readdcld 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) + C ) e. RR )
64 7 rpcnd 
 |-  ( ph -> U e. CC )
65 58 recnd 
 |-  ( ph -> ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) e. CC )
66 29 recnd 
 |-  ( ph -> ( log ` Z ) e. CC )
67 64 65 66 subdird 
 |-  ( ph -> ( ( U - ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) ) x. ( log ` Z ) ) = ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
68 43 rpcnd 
 |-  ( ph -> L e. CC )
69 47 rpcnd 
 |-  ( ph -> ( E ^ 2 ) e. CC )
70 55 rpcnne0d 
 |-  ( ph -> ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) )
71 div23 
 |-  ( ( L e. CC /\ ( E ^ 2 ) e. CC /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) = ( ( L / ( ; 3 2 x. B ) ) x. ( E ^ 2 ) ) )
72 68 69 70 71 syl3anc 
 |-  ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) = ( ( L / ( ; 3 2 x. B ) ) x. ( E ^ 2 ) ) )
73 9 oveq1i 
 |-  ( E ^ 2 ) = ( ( U / D ) ^ 2 )
74 42 simp2d 
 |-  ( ph -> D e. RR+ )
75 74 rpcnd 
 |-  ( ph -> D e. CC )
76 74 rpne0d 
 |-  ( ph -> D =/= 0 )
77 64 75 76 sqdivd 
 |-  ( ph -> ( ( U / D ) ^ 2 ) = ( ( U ^ 2 ) / ( D ^ 2 ) ) )
78 73 77 syl5eq 
 |-  ( ph -> ( E ^ 2 ) = ( ( U ^ 2 ) / ( D ^ 2 ) ) )
79 78 oveq2d 
 |-  ( ph -> ( ( L / ( ; 3 2 x. B ) ) x. ( E ^ 2 ) ) = ( ( L / ( ; 3 2 x. B ) ) x. ( ( U ^ 2 ) / ( D ^ 2 ) ) ) )
80 43 55 rpdivcld 
 |-  ( ph -> ( L / ( ; 3 2 x. B ) ) e. RR+ )
81 80 rpcnd 
 |-  ( ph -> ( L / ( ; 3 2 x. B ) ) e. CC )
82 64 sqcld 
 |-  ( ph -> ( U ^ 2 ) e. CC )
83 rpexpcl 
 |-  ( ( D e. RR+ /\ 2 e. ZZ ) -> ( D ^ 2 ) e. RR+ )
84 74 45 83 sylancl 
 |-  ( ph -> ( D ^ 2 ) e. RR+ )
85 84 rpcnne0d 
 |-  ( ph -> ( ( D ^ 2 ) e. CC /\ ( D ^ 2 ) =/= 0 ) )
86 divass 
 |-  ( ( ( L / ( ; 3 2 x. B ) ) e. CC /\ ( U ^ 2 ) e. CC /\ ( ( D ^ 2 ) e. CC /\ ( D ^ 2 ) =/= 0 ) ) -> ( ( ( L / ( ; 3 2 x. B ) ) x. ( U ^ 2 ) ) / ( D ^ 2 ) ) = ( ( L / ( ; 3 2 x. B ) ) x. ( ( U ^ 2 ) / ( D ^ 2 ) ) ) )
87 div23 
 |-  ( ( ( L / ( ; 3 2 x. B ) ) e. CC /\ ( U ^ 2 ) e. CC /\ ( ( D ^ 2 ) e. CC /\ ( D ^ 2 ) =/= 0 ) ) -> ( ( ( L / ( ; 3 2 x. B ) ) x. ( U ^ 2 ) ) / ( D ^ 2 ) ) = ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) )
88 86 87 eqtr3d 
 |-  ( ( ( L / ( ; 3 2 x. B ) ) e. CC /\ ( U ^ 2 ) e. CC /\ ( ( D ^ 2 ) e. CC /\ ( D ^ 2 ) =/= 0 ) ) -> ( ( L / ( ; 3 2 x. B ) ) x. ( ( U ^ 2 ) / ( D ^ 2 ) ) ) = ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) )
89 81 82 85 88 syl3anc 
 |-  ( ph -> ( ( L / ( ; 3 2 x. B ) ) x. ( ( U ^ 2 ) / ( D ^ 2 ) ) ) = ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) )
90 72 79 89 3eqtrd 
 |-  ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) = ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) )
91 90 oveq2d 
 |-  ( ph -> ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) = ( ( U - E ) x. ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) ) )
92 df-3 
 |-  3 = ( 2 + 1 )
93 92 oveq2i 
 |-  ( U ^ 3 ) = ( U ^ ( 2 + 1 ) )
94 2nn0 
 |-  2 e. NN0
95 expp1 
 |-  ( ( U e. CC /\ 2 e. NN0 ) -> ( U ^ ( 2 + 1 ) ) = ( ( U ^ 2 ) x. U ) )
96 64 94 95 sylancl 
 |-  ( ph -> ( U ^ ( 2 + 1 ) ) = ( ( U ^ 2 ) x. U ) )
97 93 96 syl5eq 
 |-  ( ph -> ( U ^ 3 ) = ( ( U ^ 2 ) x. U ) )
98 82 64 mulcomd 
 |-  ( ph -> ( ( U ^ 2 ) x. U ) = ( U x. ( U ^ 2 ) ) )
99 97 98 eqtrd 
 |-  ( ph -> ( U ^ 3 ) = ( U x. ( U ^ 2 ) ) )
100 99 oveq2d 
 |-  ( ph -> ( F x. ( U ^ 3 ) ) = ( F x. ( U x. ( U ^ 2 ) ) ) )
101 42 simp3d 
 |-  ( ph -> F e. RR+ )
102 101 rpcnd 
 |-  ( ph -> F e. CC )
103 102 64 82 mulassd 
 |-  ( ph -> ( ( F x. U ) x. ( U ^ 2 ) ) = ( F x. ( U x. ( U ^ 2 ) ) ) )
104 1cnd 
 |-  ( ph -> 1 e. CC )
105 74 rpreccld 
 |-  ( ph -> ( 1 / D ) e. RR+ )
106 105 rpcnd 
 |-  ( ph -> ( 1 / D ) e. CC )
107 104 106 64 subdird 
 |-  ( ph -> ( ( 1 - ( 1 / D ) ) x. U ) = ( ( 1 x. U ) - ( ( 1 / D ) x. U ) ) )
108 64 mulid2d 
 |-  ( ph -> ( 1 x. U ) = U )
109 64 75 76 divrec2d 
 |-  ( ph -> ( U / D ) = ( ( 1 / D ) x. U ) )
110 9 109 eqtr2id 
 |-  ( ph -> ( ( 1 / D ) x. U ) = E )
111 108 110 oveq12d 
 |-  ( ph -> ( ( 1 x. U ) - ( ( 1 / D ) x. U ) ) = ( U - E ) )
112 107 111 eqtr2d 
 |-  ( ph -> ( U - E ) = ( ( 1 - ( 1 / D ) ) x. U ) )
113 112 oveq1d 
 |-  ( ph -> ( ( U - E ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) = ( ( ( 1 - ( 1 / D ) ) x. U ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) )
114 6 oveq1i 
 |-  ( F x. U ) = ( ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) x. U )
115 104 106 subcld 
 |-  ( ph -> ( 1 - ( 1 / D ) ) e. CC )
116 80 84 rpdivcld 
 |-  ( ph -> ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) e. RR+ )
117 116 rpcnd 
 |-  ( ph -> ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) e. CC )
118 115 117 64 mul32d 
 |-  ( ph -> ( ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) x. U ) = ( ( ( 1 - ( 1 / D ) ) x. U ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) )
119 114 118 syl5eq 
 |-  ( ph -> ( F x. U ) = ( ( ( 1 - ( 1 / D ) ) x. U ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) )
120 113 119 eqtr4d 
 |-  ( ph -> ( ( U - E ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) = ( F x. U ) )
121 120 oveq1d 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) x. ( U ^ 2 ) ) = ( ( F x. U ) x. ( U ^ 2 ) ) )
122 40 rpcnd 
 |-  ( ph -> ( U - E ) e. CC )
123 122 117 82 mulassd 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) x. ( U ^ 2 ) ) = ( ( U - E ) x. ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) ) )
124 121 123 eqtr3d 
 |-  ( ph -> ( ( F x. U ) x. ( U ^ 2 ) ) = ( ( U - E ) x. ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) ) )
125 100 103 124 3eqtr2d 
 |-  ( ph -> ( F x. ( U ^ 3 ) ) = ( ( U - E ) x. ( ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) x. ( U ^ 2 ) ) ) )
126 91 125 eqtr4d 
 |-  ( ph -> ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) = ( F x. ( U ^ 3 ) ) )
127 126 oveq2d 
 |-  ( ph -> ( U - ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) ) = ( U - ( F x. ( U ^ 3 ) ) ) )
128 127 oveq1d 
 |-  ( ph -> ( ( U - ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) ) x. ( log ` Z ) ) = ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) )
129 67 128 eqtr3d 
 |-  ( ph -> ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) = ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) )
130 31 29 remulcld 
 |-  ( ph -> ( U x. ( log ` Z ) ) e. RR )
131 130 59 resubcld 
 |-  ( ph -> ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) e. RR )
132 129 131 eqeltrrd 
 |-  ( ph -> ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) e. RR )
133 22 rpred 
 |-  ( ph -> Z e. RR )
134 21 simp2d 
 |-  ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
135 134 simp1d 
 |-  ( ph -> 1 < Z )
136 133 135 rplogcld 
 |-  ( ph -> ( log ` Z ) e. RR+ )
137 37 136 rerpdivcld 
 |-  ( ph -> ( 2 / ( log ` Z ) ) e. RR )
138 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( Z / Y ) ) ) e. Fin )
139 22 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> Z e. RR+ )
140 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n e. NN )
141 140 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. NN )
142 141 nnrpd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. RR+ )
143 139 142 rpdivcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( Z / n ) e. RR+ )
144 23 ffvelrni 
 |-  ( ( Z / n ) e. RR+ -> ( R ` ( Z / n ) ) e. RR )
145 143 144 syl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( R ` ( Z / n ) ) e. RR )
146 145 139 rerpdivcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( R ` ( Z / n ) ) / Z ) e. RR )
147 146 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC )
148 147 abscld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR )
149 142 relogcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. RR )
150 148 149 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) e. RR )
151 138 150 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) e. RR )
152 137 151 remulcld 
 |-  ( ph -> ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) e. RR )
153 152 62 readdcld 
 |-  ( ph -> ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) + C ) e. RR )
154 25 recnd 
 |-  ( ph -> ( R ` Z ) e. CC )
155 154 abscld 
 |-  ( ph -> ( abs ` ( R ` Z ) ) e. RR )
156 155 recnd 
 |-  ( ph -> ( abs ` ( R ` Z ) ) e. CC )
157 156 66 mulcld 
 |-  ( ph -> ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) e. CC )
158 137 recnd 
 |-  ( ph -> ( 2 / ( log ` Z ) ) e. CC )
159 145 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( R ` ( Z / n ) ) e. CC )
160 159 abscld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( R ` ( Z / n ) ) ) e. RR )
161 160 149 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) e. RR )
162 138 161 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) e. RR )
163 162 recnd 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) e. CC )
164 158 163 mulcld 
 |-  ( ph -> ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) e. CC )
165 22 rpcnd 
 |-  ( ph -> Z e. CC )
166 22 rpne0d 
 |-  ( ph -> Z =/= 0 )
167 157 164 165 166 divsubdird 
 |-  ( ph -> ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) / Z ) = ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) / Z ) - ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) / Z ) ) )
168 156 66 165 166 div23d 
 |-  ( ph -> ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) / Z ) = ( ( ( abs ` ( R ` Z ) ) / Z ) x. ( log ` Z ) ) )
169 154 165 166 absdivd 
 |-  ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) = ( ( abs ` ( R ` Z ) ) / ( abs ` Z ) ) )
170 22 rprege0d 
 |-  ( ph -> ( Z e. RR /\ 0 <_ Z ) )
171 absid 
 |-  ( ( Z e. RR /\ 0 <_ Z ) -> ( abs ` Z ) = Z )
172 170 171 syl 
 |-  ( ph -> ( abs ` Z ) = Z )
173 172 oveq2d 
 |-  ( ph -> ( ( abs ` ( R ` Z ) ) / ( abs ` Z ) ) = ( ( abs ` ( R ` Z ) ) / Z ) )
174 169 173 eqtrd 
 |-  ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) = ( ( abs ` ( R ` Z ) ) / Z ) )
175 174 oveq1d 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) = ( ( ( abs ` ( R ` Z ) ) / Z ) x. ( log ` Z ) ) )
176 168 175 eqtr4d 
 |-  ( ph -> ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) / Z ) = ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) )
177 158 163 165 166 divassd 
 |-  ( ph -> ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) / Z ) = ( ( 2 / ( log ` Z ) ) x. ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) ) )
178 165 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> Z e. CC )
179 166 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> Z =/= 0 )
180 159 178 179 absdivd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) = ( ( abs ` ( R ` ( Z / n ) ) ) / ( abs ` Z ) ) )
181 172 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` Z ) = Z )
182 181 oveq2d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( R ` ( Z / n ) ) ) / ( abs ` Z ) ) = ( ( abs ` ( R ` ( Z / n ) ) ) / Z ) )
183 180 182 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) = ( ( abs ` ( R ` ( Z / n ) ) ) / Z ) )
184 183 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) = ( ( ( abs ` ( R ` ( Z / n ) ) ) / Z ) x. ( log ` n ) ) )
185 160 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( R ` ( Z / n ) ) ) e. CC )
186 149 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. CC )
187 22 rpcnne0d 
 |-  ( ph -> ( Z e. CC /\ Z =/= 0 ) )
188 187 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( Z e. CC /\ Z =/= 0 ) )
189 div23 
 |-  ( ( ( abs ` ( R ` ( Z / n ) ) ) e. CC /\ ( log ` n ) e. CC /\ ( Z e. CC /\ Z =/= 0 ) ) -> ( ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) = ( ( ( abs ` ( R ` ( Z / n ) ) ) / Z ) x. ( log ` n ) ) )
190 185 186 188 189 syl3anc 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) = ( ( ( abs ` ( R ` ( Z / n ) ) ) / Z ) x. ( log ` n ) ) )
191 184 190 eqtr4d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) = ( ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) )
192 191 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) )
193 161 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) e. CC )
194 138 165 193 166 fsumdivc 
 |-  ( ph -> ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) )
195 192 194 eqtr4d 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) )
196 195 oveq2d 
 |-  ( ph -> ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) = ( ( 2 / ( log ` Z ) ) x. ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) / Z ) ) )
197 177 196 eqtr4d 
 |-  ( ph -> ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) / Z ) = ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
198 176 197 oveq12d 
 |-  ( ph -> ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) / Z ) - ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) / Z ) ) = ( ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
199 167 198 eqtrd 
 |-  ( ph -> ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) / Z ) = ( ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
200 2fveq3 
 |-  ( z = Z -> ( abs ` ( R ` z ) ) = ( abs ` ( R ` Z ) ) )
201 fveq2 
 |-  ( z = Z -> ( log ` z ) = ( log ` Z ) )
202 200 201 oveq12d 
 |-  ( z = Z -> ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) = ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) )
203 201 oveq2d 
 |-  ( z = Z -> ( 2 / ( log ` z ) ) = ( 2 / ( log ` Z ) ) )
204 oveq2 
 |-  ( i = n -> ( z / i ) = ( z / n ) )
205 204 fveq2d 
 |-  ( i = n -> ( R ` ( z / i ) ) = ( R ` ( z / n ) ) )
206 205 fveq2d 
 |-  ( i = n -> ( abs ` ( R ` ( z / i ) ) ) = ( abs ` ( R ` ( z / n ) ) ) )
207 fveq2 
 |-  ( i = n -> ( log ` i ) = ( log ` n ) )
208 206 207 oveq12d 
 |-  ( i = n -> ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) = ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) )
209 208 cbvsumv 
 |-  sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) = sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) )
210 fvoveq1 
 |-  ( z = Z -> ( |_ ` ( z / Y ) ) = ( |_ ` ( Z / Y ) ) )
211 210 oveq2d 
 |-  ( z = Z -> ( 1 ... ( |_ ` ( z / Y ) ) ) = ( 1 ... ( |_ ` ( Z / Y ) ) ) )
212 simpl 
 |-  ( ( z = Z /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> z = Z )
213 212 fvoveq1d 
 |-  ( ( z = Z /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( R ` ( z / n ) ) = ( R ` ( Z / n ) ) )
214 213 fveq2d 
 |-  ( ( z = Z /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( R ` ( z / n ) ) ) = ( abs ` ( R ` ( Z / n ) ) ) )
215 214 oveq1d 
 |-  ( ( z = Z /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) = ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) )
216 211 215 sumeq12rdv 
 |-  ( z = Z -> sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) )
217 209 216 syl5eq 
 |-  ( z = Z -> sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) )
218 203 217 oveq12d 
 |-  ( z = Z -> ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) = ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) )
219 202 218 oveq12d 
 |-  ( z = Z -> ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) = ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) )
220 id 
 |-  ( z = Z -> z = Z )
221 219 220 oveq12d 
 |-  ( z = Z -> ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) = ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) / Z ) )
222 221 breq1d 
 |-  ( z = Z -> ( ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C <-> ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) / Z ) <_ C ) )
223 1re 
 |-  1 e. RR
224 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
225 elioopnf 
 |-  ( 1 e. RR* -> ( Z e. ( 1 (,) +oo ) <-> ( Z e. RR /\ 1 < Z ) ) )
226 223 224 225 mp2b 
 |-  ( Z e. ( 1 (,) +oo ) <-> ( Z e. RR /\ 1 < Z ) )
227 133 135 226 sylanbrc 
 |-  ( ph -> Z e. ( 1 (,) +oo ) )
228 222 20 227 rspcdva 
 |-  ( ph -> ( ( ( ( abs ` ( R ` Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( R ` ( Z / n ) ) ) x. ( log ` n ) ) ) ) / Z ) <_ C )
229 199 228 eqbrtrrd 
 |-  ( ph -> ( ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) <_ C )
230 30 152 62 lesubadd2d 
 |-  ( ph -> ( ( ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) - ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) <_ C <-> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) <_ ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) + C ) ) )
231 229 230 mpbid 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) <_ ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) + C ) )
232 2cnd 
 |-  ( ph -> 2 e. CC )
233 148 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. CC )
234 233 186 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) e. CC )
235 138 234 fsumcl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) e. CC )
236 136 rpne0d 
 |-  ( ph -> ( log ` Z ) =/= 0 )
237 232 235 66 236 div23d 
 |-  ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) / ( log ` Z ) ) = ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
238 29 resqcld 
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) e. RR )
239 57 238 remulcld 
 |-  ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) e. RR )
240 41 239 remulcld 
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) e. RR )
241 remulcl 
 |-  ( ( 2 e. RR /\ ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) e. RR ) -> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) e. RR )
242 36 240 241 sylancr 
 |-  ( ph -> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) e. RR )
243 35 29 remulcld 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) e. RR )
244 remulcl 
 |-  ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) e. RR )
245 36 151 244 sylancr 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) e. RR )
246 31 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> U e. RR )
247 246 141 nndivred 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( U / n ) e. RR )
248 247 148 resubcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR )
249 248 149 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
250 138 249 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
251 37 250 remulcld 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) e. RR )
252 243 245 resubcld 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) e. RR )
253 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 pntlemf 
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
254 2pos 
 |-  0 < 2
255 254 a1i 
 |-  ( ph -> 0 < 2 )
256 lemul2 
 |-  ( ( ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) <_ ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
257 240 250 37 255 256 syl112anc 
 |-  ( ph -> ( ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) <_ ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
258 253 257 mpbid 
 |-  ( ph -> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) <_ ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
259 247 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( U / n ) e. CC )
260 259 233 186 subdird 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = ( ( ( U / n ) x. ( log ` n ) ) - ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
261 260 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) x. ( log ` n ) ) - ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
262 247 149 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) x. ( log ` n ) ) e. RR )
263 262 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) x. ( log ` n ) ) e. CC )
264 138 263 234 fsumsub 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) x. ( log ` n ) ) - ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
265 261 264 eqtrd 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) )
266 265 oveq2d 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
267 138 262 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) e. RR )
268 267 recnd 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) e. CC )
269 232 268 235 subdid 
 |-  ( ph -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
270 266 269 eqtrd 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
271 remulcl 
 |-  ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) e. RR )
272 36 267 271 sylancr 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) e. RR )
273 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 pntlemk 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )
274 272 243 245 273 lesub1dd 
 |-  ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
275 270 274 eqbrtrd 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
276 242 251 252 258 275 letrd 
 |-  ( ph -> ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) ) )
277 242 243 245 276 lesubd 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) ) )
278 35 recnd 
 |-  ( ph -> ( U x. ( ( log ` Z ) + 3 ) ) e. CC )
279 60 recnd 
 |-  ( ph -> ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) e. CC )
280 278 279 66 subdird 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) x. ( log ` Z ) ) = ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) x. ( log ` Z ) ) ) )
281 59 recnd 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) e. CC )
282 232 281 66 mulassd 
 |-  ( ph -> ( ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) x. ( log ` Z ) ) = ( 2 x. ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) ) )
283 65 66 66 mulassd 
 |-  ( ph -> ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) = ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( ( log ` Z ) x. ( log ` Z ) ) ) )
284 66 sqvald 
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) = ( ( log ` Z ) x. ( log ` Z ) ) )
285 284 oveq2d 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( ( log ` Z ) ^ 2 ) ) = ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( ( log ` Z ) x. ( log ` Z ) ) ) )
286 56 rpcnd 
 |-  ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) e. CC )
287 238 recnd 
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) e. CC )
288 122 286 287 mulassd 
 |-  ( ph -> ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( ( log ` Z ) ^ 2 ) ) = ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) )
289 283 285 288 3eqtr2d 
 |-  ( ph -> ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) = ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) )
290 289 oveq2d 
 |-  ( ph -> ( 2 x. ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) ) = ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) )
291 282 290 eqtrd 
 |-  ( ph -> ( ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) x. ( log ` Z ) ) = ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) )
292 291 oveq2d 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) x. ( log ` Z ) ) ) = ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) ) )
293 280 292 eqtrd 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) x. ( log ` Z ) ) = ( ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) - ( 2 x. ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) ) ) )
294 277 293 breqtrrd 
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) x. ( log ` Z ) ) )
295 245 61 136 ledivmul2d 
 |-  ( ph -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) / ( log ` Z ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) <-> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) x. ( log ` Z ) ) ) )
296 294 295 mpbird 
 |-  ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) / ( log ` Z ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
297 237 296 eqbrtrrd 
 |-  ( ph -> ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
298 152 61 62 297 leadd1dd 
 |-  ( ph -> ( ( ( 2 / ( log ` Z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( log ` n ) ) ) + C ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) + C ) )
299 30 153 63 231 298 letrd 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) <_ ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) + C ) )
300 remulcl 
 |-  ( ( U e. RR /\ 3 e. RR ) -> ( U x. 3 ) e. RR )
301 31 32 300 sylancl 
 |-  ( ph -> ( U x. 3 ) e. RR )
302 301 62 readdcld 
 |-  ( ph -> ( ( U x. 3 ) + C ) e. RR )
303 21 simp3d 
 |-  ( ph -> ( ( 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 ) ) ) )
304 303 simp3d 
 |-  ( ph -> ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) )
305 302 59 130 304 leadd2dd 
 |-  ( ph -> ( ( U x. ( log ` Z ) ) + ( ( U x. 3 ) + C ) ) <_ ( ( U x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
306 33 recnd 
 |-  ( ph -> 3 e. CC )
307 64 66 306 adddid 
 |-  ( ph -> ( U x. ( ( log ` Z ) + 3 ) ) = ( ( U x. ( log ` Z ) ) + ( U x. 3 ) ) )
308 307 oveq1d 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) = ( ( ( U x. ( log ` Z ) ) + ( U x. 3 ) ) + C ) )
309 130 recnd 
 |-  ( ph -> ( U x. ( log ` Z ) ) e. CC )
310 64 306 mulcld 
 |-  ( ph -> ( U x. 3 ) e. CC )
311 13 rpcnd 
 |-  ( ph -> C e. CC )
312 309 310 311 addassd 
 |-  ( ph -> ( ( ( U x. ( log ` Z ) ) + ( U x. 3 ) ) + C ) = ( ( U x. ( log ` Z ) ) + ( ( U x. 3 ) + C ) ) )
313 308 312 eqtrd 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) = ( ( U x. ( log ` Z ) ) + ( ( U x. 3 ) + C ) ) )
314 281 2timesd 
 |-  ( ph -> ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) = ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
315 314 oveq2d 
 |-  ( ph -> ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) = ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
316 309 281 281 nppcan3d 
 |-  ( ph -> ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) = ( ( U x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
317 315 316 eqtrd 
 |-  ( ph -> ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) = ( ( U x. ( log ` Z ) ) + ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
318 305 313 317 3brtr4d 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) <_ ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
319 35 62 readdcld 
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) e. RR )
320 319 60 131 lesubaddd 
 |-  ( ph -> ( ( ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) <_ ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) <-> ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) <_ ( ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) + ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) ) )
321 318 320 mpbird 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) <_ ( ( U x. ( log ` Z ) ) - ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
322 278 311 279 addsubd 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) + C ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) = ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) + C ) )
323 321 322 129 3brtr3d 
 |-  ( ph -> ( ( ( U x. ( ( log ` Z ) + 3 ) ) - ( 2 x. ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) + C ) <_ ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) )
324 30 63 132 299 323 letrd 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) <_ ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) )
325 3z 
 |-  3 e. ZZ
326 rpexpcl 
 |-  ( ( U e. RR+ /\ 3 e. ZZ ) -> ( U ^ 3 ) e. RR+ )
327 7 325 326 sylancl 
 |-  ( ph -> ( U ^ 3 ) e. RR+ )
328 101 327 rpmulcld 
 |-  ( ph -> ( F x. ( U ^ 3 ) ) e. RR+ )
329 328 rpred 
 |-  ( ph -> ( F x. ( U ^ 3 ) ) e. RR )
330 31 329 resubcld 
 |-  ( ph -> ( U - ( F x. ( U ^ 3 ) ) ) e. RR )
331 28 330 136 lemul1d 
 |-  ( ph -> ( ( abs ` ( ( R ` Z ) / Z ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) <-> ( ( abs ` ( ( R ` Z ) / Z ) ) x. ( log ` Z ) ) <_ ( ( U - ( F x. ( U ^ 3 ) ) ) x. ( log ` Z ) ) ) )
332 324 331 mpbird 
 |-  ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )