Metamath Proof Explorer

Theorem logexprlim

Description: The sum sum_ n <_ x , log ^ N ( x / n ) has the asymptotic expansion ( N ! ) x + o ( x ) . (More precisely, the omitted term has order O ( log ^ N ( x ) / x ) .) (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Assertion logexprlim 
|- ( N e. NN0 -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) ) ~~>r ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
2 simpr 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> x e. RR+ )
3 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
4 3 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
5 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
6 2 4 5 syl2an 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
7 6 relogcld 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
8 simpll 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN0 )
9 7 8 reexpcld 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ N ) e. RR )
10 1 9 fsumrecl 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) e. RR )
11 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
12 id 
 |-  ( N e. NN0 -> N e. NN0 )
13 reexpcl 
 |-  ( ( ( log ` x ) e. RR /\ N e. NN0 ) -> ( ( log ` x ) ^ N ) e. RR )
14 11 12 13 syl2anr 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( log ` x ) ^ N ) e. RR )
15 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
16 15 adantr 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ! ` N ) e. NN )
17 16 nnred 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ! ` N ) e. RR )
18 fzfid 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( 0 ... N ) e. Fin )
19 11 adantl 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( log ` x ) e. RR )
20 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
21 reexpcl 
 |-  ( ( ( log ` x ) e. RR /\ k e. NN0 ) -> ( ( log ` x ) ^ k ) e. RR )
22 19 20 21 syl2an 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( log ` x ) ^ k ) e. RR )
23 20 adantl 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
24 23 faccld 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
25 22 24 nndivred 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. RR )
26 18 25 fsumrecl 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. RR )
27 17 26 remulcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) e. RR )
28 14 27 resubcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. RR )
29 10 28 resubcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) e. RR )
30 29 2 rerpdivcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) e. RR )
31 rerpdivcl 
 |-  ( ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. RR /\ x e. RR+ ) -> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) e. RR )
32 28 31 sylancom 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) e. RR )
33 1red 
 |-  ( N e. NN0 -> 1 e. RR )
34 15 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
35 simpl 
 |-  ( ( k = N /\ x e. RR+ ) -> k = N )
36 35 oveq2d 
 |-  ( ( k = N /\ x e. RR+ ) -> ( ( log ` x ) ^ k ) = ( ( log ` x ) ^ N ) )
37 36 oveq1d 
 |-  ( ( k = N /\ x e. RR+ ) -> ( ( ( log ` x ) ^ k ) / x ) = ( ( ( log ` x ) ^ N ) / x ) )
38 37 mpteq2dva 
 |-  ( k = N -> ( x e. RR+ |-> ( ( ( log ` x ) ^ k ) / x ) ) = ( x e. RR+ |-> ( ( ( log ` x ) ^ N ) / x ) ) )
39 38 breq1d 
 |-  ( k = N -> ( ( x e. RR+ |-> ( ( ( log ` x ) ^ k ) / x ) ) ~~>r 0 <-> ( x e. RR+ |-> ( ( ( log ` x ) ^ N ) / x ) ) ~~>r 0 ) )
40 11 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
41 id 
 |-  ( k e. NN0 -> k e. NN0 )
42 cxpexp 
 |-  ( ( ( log ` x ) e. CC /\ k e. NN0 ) -> ( ( log ` x ) ^c k ) = ( ( log ` x ) ^ k ) )
43 40 41 42 syl2anr 
 |-  ( ( k e. NN0 /\ x e. RR+ ) -> ( ( log ` x ) ^c k ) = ( ( log ` x ) ^ k ) )
44 rpcn 
 |-  ( x e. RR+ -> x e. CC )
45 44 adantl 
 |-  ( ( k e. NN0 /\ x e. RR+ ) -> x e. CC )
46 45 cxp1d 
 |-  ( ( k e. NN0 /\ x e. RR+ ) -> ( x ^c 1 ) = x )
47 43 46 oveq12d 
 |-  ( ( k e. NN0 /\ x e. RR+ ) -> ( ( ( log ` x ) ^c k ) / ( x ^c 1 ) ) = ( ( ( log ` x ) ^ k ) / x ) )
48 47 mpteq2dva 
 |-  ( k e. NN0 -> ( x e. RR+ |-> ( ( ( log ` x ) ^c k ) / ( x ^c 1 ) ) ) = ( x e. RR+ |-> ( ( ( log ` x ) ^ k ) / x ) ) )
49 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
50 1rp 
 |-  1 e. RR+
51 cxploglim2 
 |-  ( ( k e. CC /\ 1 e. RR+ ) -> ( x e. RR+ |-> ( ( ( log ` x ) ^c k ) / ( x ^c 1 ) ) ) ~~>r 0 )
52 49 50 51 sylancl 
 |-  ( k e. NN0 -> ( x e. RR+ |-> ( ( ( log ` x ) ^c k ) / ( x ^c 1 ) ) ) ~~>r 0 )
53 48 52 eqbrtrrd 
 |-  ( k e. NN0 -> ( x e. RR+ |-> ( ( ( log ` x ) ^ k ) / x ) ) ~~>r 0 )
54 39 53 vtoclga 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( log ` x ) ^ N ) / x ) ) ~~>r 0 )
55 rerpdivcl 
 |-  ( ( ( ( log ` x ) ^ N ) e. RR /\ x e. RR+ ) -> ( ( ( log ` x ) ^ N ) / x ) e. RR )
56 14 55 sylancom 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( log ` x ) ^ N ) / x ) e. RR )
57 56 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( log ` x ) ^ N ) / x ) e. CC )
58 10 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) e. CC )
59 14 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( log ` x ) ^ N ) e. CC )
60 34 adantr 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ! ` N ) e. CC )
61 26 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC )
62 60 61 mulcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) e. CC )
63 59 62 subcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. CC )
64 58 63 subcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) e. CC )
65 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
66 65 adantl 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( x e. CC /\ x =/= 0 ) )
67 66 simpld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> x e. CC )
68 66 simprd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> x =/= 0 )
69 64 67 68 divcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) e. CC )
70 69 adantrr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) e. CC )
71 15 adantr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ! ` N ) e. NN )
72 71 nncnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ! ` N ) e. CC )
73 70 72 subcld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) e. CC )
74 73 abscld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) e. RR )
75 56 adantrr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) / x ) e. RR )
76 75 recnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) / x ) e. CC )
77 76 abscld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( log ` x ) ^ N ) / x ) ) e. RR )
78 ioorp 
 |-  ( 0 (,) +oo ) = RR+
79 78 eqcomi 
 |-  RR+ = ( 0 (,) +oo )
80 nnuz 
 |-  NN = ( ZZ>= ` 1 )
81 1z 
 |-  1 e. ZZ
82 81 a1i 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. ZZ )
83 1red 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. RR )
84 1re 
 |-  1 e. RR
85 1nn0 
 |-  1 e. NN0
86 84 85 nn0addge1i 
 |-  1 <_ ( 1 + 1 )
87 86 a1i 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ ( 1 + 1 ) )
88 0red 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 e. RR )
89 71 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ! ` N ) e. NN )
90 89 nnred 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ! ` N ) e. RR )
91 rpre 
 |-  ( y e. RR+ -> y e. RR )
92 91 adantl 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> y e. RR )
93 fzfid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( 0 ... N ) e. Fin )
94 simprl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
95 rpdivcl 
 |-  ( ( x e. RR+ /\ y e. RR+ ) -> ( x / y ) e. RR+ )
96 94 95 sylan 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( x / y ) e. RR+ )
97 96 relogcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( log ` ( x / y ) ) e. RR )
98 reexpcl 
 |-  ( ( ( log ` ( x / y ) ) e. RR /\ k e. NN0 ) -> ( ( log ` ( x / y ) ) ^ k ) e. RR )
99 97 20 98 syl2an 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( log ` ( x / y ) ) ^ k ) e. RR )
100 20 adantl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
101 100 faccld 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
102 99 101 nndivred 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) e. RR )
103 93 102 fsumrecl 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) e. RR )
104 92 103 remulcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) e. RR )
105 90 104 remulcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) e. RR )
106 simpll 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> N e. NN0 )
107 97 106 reexpcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ( log ` ( x / y ) ) ^ N ) e. RR )
108 nnrp 
 |-  ( y e. NN -> y e. RR+ )
109 108 107 sylan2 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. NN ) -> ( ( log ` ( x / y ) ) ^ N ) e. RR )
110 reelprrecn 
 |-  RR e. { RR , CC }
111 110 a1i 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> RR e. { RR , CC } )
112 104 recnd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) e. CC )
113 107 89 nndivred 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) e. RR )
114 simpl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> N e. NN0 )
115 advlogexp 
 |-  ( ( x e. RR+ /\ N e. NN0 ) -> ( RR _D ( y e. RR+ |-> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( y e. RR+ |-> ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) ) )
116 94 114 115 syl2anc 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( RR _D ( y e. RR+ |-> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( y e. RR+ |-> ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) ) )
117 111 112 113 116 72 dvmptcmul 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( RR _D ( y e. RR+ |-> ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) = ( y e. RR+ |-> ( ( ! ` N ) x. ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) ) ) )
118 107 recnd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ( log ` ( x / y ) ) ^ N ) e. CC )
119 72 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ! ` N ) e. CC )
120 71 nnne0d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ! ` N ) =/= 0 )
121 120 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ! ` N ) =/= 0 )
122 118 119 121 divcan2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> ( ( ! ` N ) x. ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) ) = ( ( log ` ( x / y ) ) ^ N ) )
123 122 mpteq2dva 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( y e. RR+ |-> ( ( ! ` N ) x. ( ( ( log ` ( x / y ) ) ^ N ) / ( ! ` N ) ) ) ) = ( y e. RR+ |-> ( ( log ` ( x / y ) ) ^ N ) ) )
124 117 123 eqtrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( RR _D ( y e. RR+ |-> ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) = ( y e. RR+ |-> ( ( log ` ( x / y ) ) ^ N ) ) )
125 oveq2 
 |-  ( y = n -> ( x / y ) = ( x / n ) )
126 125 fveq2d 
 |-  ( y = n -> ( log ` ( x / y ) ) = ( log ` ( x / n ) ) )
127 126 oveq1d 
 |-  ( y = n -> ( ( log ` ( x / y ) ) ^ N ) = ( ( log ` ( x / n ) ) ^ N ) )
128 94 rpxrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR* )
129 simp1rl 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> x e. RR+ )
130 simp2r 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> n e. RR+ )
131 129 130 rpdivcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( x / n ) e. RR+ )
132 131 relogcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( log ` ( x / n ) ) e. RR )
133 simp2l 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> y e. RR+ )
134 129 133 rpdivcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( x / y ) e. RR+ )
135 134 relogcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( log ` ( x / y ) ) e. RR )
136 simp1l 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> N e. NN0 )
137 log1 
 |-  ( log ` 1 ) = 0
138 130 rpcnd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> n e. CC )
139 138 mullidd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( 1 x. n ) = n )
140 simp33 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> n <_ x )
141 139 140 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( 1 x. n ) <_ x )
142 1red 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> 1 e. RR )
143 129 rpred 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> x e. RR )
144 142 143 130 lemuldivd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
145 141 144 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> 1 <_ ( x / n ) )
146 logleb 
 |-  ( ( 1 e. RR+ /\ ( x / n ) e. RR+ ) -> ( 1 <_ ( x / n ) <-> ( log ` 1 ) <_ ( log ` ( x / n ) ) ) )
147 50 131 146 sylancr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( 1 <_ ( x / n ) <-> ( log ` 1 ) <_ ( log ` ( x / n ) ) ) )
148 145 147 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( log ` 1 ) <_ ( log ` ( x / n ) ) )
149 137 148 eqbrtrrid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> 0 <_ ( log ` ( x / n ) ) )
150 simp32 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> y <_ n )
151 133 130 129 lediv2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( y <_ n <-> ( x / n ) <_ ( x / y ) ) )
152 150 151 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( x / n ) <_ ( x / y ) )
153 131 134 logled 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( ( x / n ) <_ ( x / y ) <-> ( log ` ( x / n ) ) <_ ( log ` ( x / y ) ) ) )
154 152 153 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( log ` ( x / n ) ) <_ ( log ` ( x / y ) ) )
155 leexp1a 
 |-  ( ( ( ( log ` ( x / n ) ) e. RR /\ ( log ` ( x / y ) ) e. RR /\ N e. NN0 ) /\ ( 0 <_ ( log ` ( x / n ) ) /\ ( log ` ( x / n ) ) <_ ( log ` ( x / y ) ) ) ) -> ( ( log ` ( x / n ) ) ^ N ) <_ ( ( log ` ( x / y ) ) ^ N ) )
156 132 135 136 149 154 155 syl32anc 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ n e. RR+ ) /\ ( 1 <_ y /\ y <_ n /\ n <_ x ) ) -> ( ( log ` ( x / n ) ) ^ N ) <_ ( ( log ` ( x / y ) ) ^ N ) )
157 eqid 
 |-  ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) = ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) )
158 96 3ad2antr1 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( x / y ) e. RR+ )
159 158 relogcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( log ` ( x / y ) ) e. RR )
160 simpll 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> N e. NN0 )
161 rpcn 
 |-  ( y e. RR+ -> y e. CC )
162 161 adantl 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y e. RR+ ) -> y e. CC )
163 162 3ad2antr1 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> y e. CC )
164 163 mullidd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( 1 x. y ) = y )
165 simpr3 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> y <_ x )
166 164 165 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( 1 x. y ) <_ x )
167 1red 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> 1 e. RR )
168 94 rpred 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
169 168 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> x e. RR )
170 simpr1 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> y e. RR+ )
171 167 169 170 lemuldivd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( ( 1 x. y ) <_ x <-> 1 <_ ( x / y ) ) )
172 166 171 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> 1 <_ ( x / y ) )
173 logleb 
 |-  ( ( 1 e. RR+ /\ ( x / y ) e. RR+ ) -> ( 1 <_ ( x / y ) <-> ( log ` 1 ) <_ ( log ` ( x / y ) ) ) )
174 50 158 173 sylancr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( 1 <_ ( x / y ) <-> ( log ` 1 ) <_ ( log ` ( x / y ) ) ) )
175 172 174 mpbid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> ( log ` 1 ) <_ ( log ` ( x / y ) ) )
176 137 175 eqbrtrrid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> 0 <_ ( log ` ( x / y ) ) )
177 159 160 176 expge0d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( y e. RR+ /\ 1 <_ y /\ y <_ x ) ) -> 0 <_ ( ( log ` ( x / y ) ) ^ N ) )
178 50 a1i 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. RR+ )
179 1le1 
 |-  1 <_ 1
180 179 a1i 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ 1 )
181 simprr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
182 168 leidd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x <_ x )
183 79 80 82 83 87 88 105 107 109 124 127 128 156 157 177 178 94 180 181 182 dvfsumlem4 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) - ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) ) ) <_ [_ 1 / y ]_ ( ( log ` ( x / y ) ) ^ N ) )
184 fzfid 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
185 94 4 5 syl2an 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
186 185 relogcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
187 simpll 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN0 )
188 186 187 reexpcld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ N ) e. RR )
189 184 188 fsumrecl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) e. RR )
190 189 recnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) e. CC )
191 94 rpcnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. CC )
192 72 191 mulcld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ! ` N ) x. x ) e. CC )
193 11 ad2antrl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. RR )
194 193 recnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. CC )
195 194 114 expcld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) ^ N ) e. CC )
196 fzfid 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 0 ... N ) e. Fin )
197 193 20 21 syl2an 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 0 ... N ) ) -> ( ( log ` x ) ^ k ) e. RR )
198 20 adantl 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
199 198 faccld 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
200 197 199 nndivred 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. RR )
201 200 recnd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC )
202 196 201 fsumcl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC )
203 72 202 mulcld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) e. CC )
204 195 203 subcld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. CC )
205 190 192 204 sub32d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. x ) ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) - ( ( ! ` N ) x. x ) ) )
206 eqidd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) = ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) )
207 simpr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> y = x )
208 207 fveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( |_ ` y ) = ( |_ ` x ) )
209 208 oveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` x ) ) )
210 209 sumeq1d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) )
211 oveq2 
 |-  ( y = x -> ( x / y ) = ( x / x ) )
212 65 ad2antrl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. CC /\ x =/= 0 ) )
213 divid 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( x / x ) = 1 )
214 212 213 syl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x / x ) = 1 )
215 211 214 sylan9eqr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( x / y ) = 1 )
216 215 adantr 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( 0 ... N ) ) -> ( x / y ) = 1 )
217 216 fveq2d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( 0 ... N ) ) -> ( log ` ( x / y ) ) = ( log ` 1 ) )
218 217 137 eqtrdi 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( 0 ... N ) ) -> ( log ` ( x / y ) ) = 0 )
219 218 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( 0 ... N ) ) -> ( ( log ` ( x / y ) ) ^ k ) = ( 0 ^ k ) )
220 219 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = ( ( 0 ^ k ) / ( ! ` k ) ) )
221 220 sumeq2dv 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... N ) ( ( 0 ^ k ) / ( ! ` k ) ) )
222 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
223 114 222 eleqtrdi 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> N e. ( ZZ>= ` 0 ) )
224 eluzfz1 
 |-  ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
225 223 224 syl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 e. ( 0 ... N ) )
226 225 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> 0 e. ( 0 ... N ) )
227 226 snssd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> { 0 } C_ ( 0 ... N ) )
228 elsni 
 |-  ( k e. { 0 } -> k = 0 )
229 228 adantl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. { 0 } ) -> k = 0 )
230 oveq2 
 |-  ( k = 0 -> ( 0 ^ k ) = ( 0 ^ 0 ) )
231 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
232 230 231 eqtrdi 
 |-  ( k = 0 -> ( 0 ^ k ) = 1 )
233 fveq2 
 |-  ( k = 0 -> ( ! ` k ) = ( ! ` 0 ) )
234 fac0 
 |-  ( ! ` 0 ) = 1
235 233 234 eqtrdi 
 |-  ( k = 0 -> ( ! ` k ) = 1 )
236 232 235 oveq12d 
 |-  ( k = 0 -> ( ( 0 ^ k ) / ( ! ` k ) ) = ( 1 / 1 ) )
237 1div1e1 
 |-  ( 1 / 1 ) = 1
238 236 237 eqtrdi 
 |-  ( k = 0 -> ( ( 0 ^ k ) / ( ! ` k ) ) = 1 )
239 229 238 syl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. { 0 } ) -> ( ( 0 ^ k ) / ( ! ` k ) ) = 1 )
240 ax-1cn 
 |-  1 e. CC
241 239 240 eqeltrdi 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. { 0 } ) -> ( ( 0 ^ k ) / ( ! ` k ) ) e. CC )
242 eldifi 
 |-  ( k e. ( ( 0 ... N ) \ { 0 } ) -> k e. ( 0 ... N ) )
243 242 adantl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> k e. ( 0 ... N ) )
244 243 20 syl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> k e. NN0 )
245 eldifsni 
 |-  ( k e. ( ( 0 ... N ) \ { 0 } ) -> k =/= 0 )
246 245 adantl 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> k =/= 0 )
247 eldifsn 
 |-  ( k e. ( NN0 \ { 0 } ) <-> ( k e. NN0 /\ k =/= 0 ) )
248 244 246 247 sylanbrc 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> k e. ( NN0 \ { 0 } ) )
249 dfn2 
 |-  NN = ( NN0 \ { 0 } )
250 248 249 eleqtrrdi 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> k e. NN )
251 250 0expd 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( 0 ^ k ) = 0 )
252 251 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( ( 0 ^ k ) / ( ! ` k ) ) = ( 0 / ( ! ` k ) ) )
253 244 faccld 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( ! ` k ) e. NN )
254 253 nncnd 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( ! ` k ) e. CC )
255 253 nnne0d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( ! ` k ) =/= 0 )
256 254 255 div0d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( 0 / ( ! ` k ) ) = 0 )
257 252 256 eqtrd 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) /\ k e. ( ( 0 ... N ) \ { 0 } ) ) -> ( ( 0 ^ k ) / ( ! ` k ) ) = 0 )
258 fzfid 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( 0 ... N ) e. Fin )
259 227 241 257 258 fsumss 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> sum_ k e. { 0 } ( ( 0 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... N ) ( ( 0 ^ k ) / ( ! ` k ) ) )
260 221 259 eqtr4d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = sum_ k e. { 0 } ( ( 0 ^ k ) / ( ! ` k ) ) )
261 0cn 
 |-  0 e. CC
262 238 sumsn 
 |-  ( ( 0 e. CC /\ 1 e. CC ) -> sum_ k e. { 0 } ( ( 0 ^ k ) / ( ! ` k ) ) = 1 )
263 261 240 262 mp2an 
 |-  sum_ k e. { 0 } ( ( 0 ^ k ) / ( ! ` k ) ) = 1
264 260 263 eqtrdi 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = 1 )
265 207 264 oveq12d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) = ( x x. 1 ) )
266 191 mulridd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. 1 ) = x )
267 266 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( x x. 1 ) = x )
268 265 267 eqtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) = x )
269 268 oveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) = ( ( ! ` N ) x. x ) )
270 210 269 oveq12d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = x ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. x ) ) )
271 ovexd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. x ) ) e. _V )
272 206 270 94 271 fvmptd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. x ) ) )
273 simpr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> y = 1 )
274 273 fveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( |_ ` y ) = ( |_ ` 1 ) )
275 flid 
 |-  ( 1 e. ZZ -> ( |_ ` 1 ) = 1 )
276 81 275 ax-mp 
 |-  ( |_ ` 1 ) = 1
277 274 276 eqtrdi 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( |_ ` y ) = 1 )
278 277 oveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... 1 ) )
279 278 sumeq1d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) = sum_ n e. ( 1 ... 1 ) ( ( log ` ( x / n ) ) ^ N ) )
280 191 div1d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x / 1 ) = x )
281 280 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( x / 1 ) = x )
282 281 fveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( log ` ( x / 1 ) ) = ( log ` x ) )
283 282 oveq1d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( ( log ` ( x / 1 ) ) ^ N ) = ( ( log ` x ) ^ N ) )
284 195 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( ( log ` x ) ^ N ) e. CC )
285 283 284 eqeltrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( ( log ` ( x / 1 ) ) ^ N ) e. CC )
286 oveq2 
 |-  ( n = 1 -> ( x / n ) = ( x / 1 ) )
287 286 fveq2d 
 |-  ( n = 1 -> ( log ` ( x / n ) ) = ( log ` ( x / 1 ) ) )
288 287 oveq1d 
 |-  ( n = 1 -> ( ( log ` ( x / n ) ) ^ N ) = ( ( log ` ( x / 1 ) ) ^ N ) )
289 288 fsum1 
 |-  ( ( 1 e. ZZ /\ ( ( log ` ( x / 1 ) ) ^ N ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( ( log ` ( x / n ) ) ^ N ) = ( ( log ` ( x / 1 ) ) ^ N ) )
290 81 285 289 sylancr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> sum_ n e. ( 1 ... 1 ) ( ( log ` ( x / n ) ) ^ N ) = ( ( log ` ( x / 1 ) ) ^ N ) )
291 279 290 283 3eqtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) = ( ( log ` x ) ^ N ) )
292 273 oveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( x / y ) = ( x / 1 ) )
293 292 281 eqtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( x / y ) = x )
294 293 fveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( log ` ( x / y ) ) = ( log ` x ) )
295 294 adantr 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) /\ k e. ( 0 ... N ) ) -> ( log ` ( x / y ) ) = ( log ` x ) )
296 295 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) /\ k e. ( 0 ... N ) ) -> ( ( log ` ( x / y ) ) ^ k ) = ( ( log ` x ) ^ k ) )
297 296 oveq1d 
 |-  ( ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) )
298 297 sumeq2dv 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) )
299 273 298 oveq12d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) = ( 1 x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) )
300 202 adantr 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC )
301 300 mullidd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( 1 x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) )
302 299 301 eqtrd 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) )
303 302 oveq2d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) )
304 291 303 oveq12d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) )
305 ovexd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. _V )
306 206 304 178 305 fvmptd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) = ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) )
307 272 306 oveq12d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) - ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. x ) ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) )
308 70 72 191 subdird 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) x. x ) = ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) x. x ) - ( ( ! ` N ) x. x ) ) )
309 64 adantrr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) e. CC )
310 212 simprd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> x =/= 0 )
311 309 191 310 divcan1d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) x. x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) )
312 311 oveq1d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) x. x ) - ( ( ! ` N ) x. x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) - ( ( ! ` N ) x. x ) ) )
313 308 312 eqtrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) x. x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) - ( ( ! ` N ) x. x ) ) )
314 205 307 313 3eqtr4d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) - ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) ) = ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) x. x ) )
315 314 fveq2d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) - ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) ) ) = ( abs ` ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) x. x ) ) )
316 73 191 absmuld 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) x. x ) ) = ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. ( abs ` x ) ) )
317 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
318 317 ad2antrl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 <_ x ) )
319 absid 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
320 318 319 syl 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` x ) = x )
321 320 oveq2d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. ( abs ` x ) ) = ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. x ) )
322 315 316 321 3eqtrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` x ) - ( ( y e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ! ` N ) x. ( y x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( x / y ) ) ^ k ) / ( ! ` k ) ) ) ) ) ) ` 1 ) ) ) = ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. x ) )
323 1cnd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. CC )
324 294 oveq1d 
 |-  ( ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) /\ y = 1 ) -> ( ( log ` ( x / y ) ) ^ N ) = ( ( log ` x ) ^ N ) )
325 323 324 csbied 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> [_ 1 / y ]_ ( ( log ` ( x / y ) ) ^ N ) = ( ( log ` x ) ^ N ) )
326 183 322 325 3brtr3d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. x ) <_ ( ( log ` x ) ^ N ) )
327 14 adantrr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) ^ N ) e. RR )
328 74 327 94 lemuldivd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) x. x ) <_ ( ( log ` x ) ^ N ) <-> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) <_ ( ( ( log ` x ) ^ N ) / x ) ) )
329 326 328 mpbid 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) <_ ( ( ( log ` x ) ^ N ) / x ) )
330 75 leabsd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) / x ) <_ ( abs ` ( ( ( log ` x ) ^ N ) / x ) ) )
331 74 75 77 329 330 letrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) <_ ( abs ` ( ( ( log ` x ) ^ N ) / x ) ) )
332 57 adantrr 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) ^ N ) / x ) e. CC )
333 332 subid1d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( log ` x ) ^ N ) / x ) - 0 ) = ( ( ( log ` x ) ^ N ) / x ) )
334 333 fveq2d 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( ( log ` x ) ^ N ) / x ) - 0 ) ) = ( abs ` ( ( ( log ` x ) ^ N ) / x ) ) )
335 331 334 breqtrrd 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) - ( ! ` N ) ) ) <_ ( abs ` ( ( ( ( log ` x ) ^ N ) / x ) - 0 ) ) )
336 33 34 54 57 69 335 rlimsqzlem 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) ) ~~>r ( ! ` N ) )
337 divsubdir 
 |-  ( ( ( ( log ` x ) ^ N ) e. CC /\ ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) = ( ( ( ( log ` x ) ^ N ) / x ) - ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) )
338 59 62 66 337 syl3anc 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) = ( ( ( ( log ` x ) ^ N ) / x ) - ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) )
339 338 mpteq2dva 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) = ( x e. RR+ |-> ( ( ( ( log ` x ) ^ N ) / x ) - ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) ) )
340 rerpdivcl 
 |-  ( ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) e. RR /\ x e. RR+ ) -> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) e. RR )
341 27 340 sylancom 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) e. RR )
342 divass 
 |-  ( ( ( ! ` N ) e. CC /\ sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) = ( ( ! ` N ) x. ( sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) ) )
343 60 61 66 342 syl3anc 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) = ( ( ! ` N ) x. ( sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) ) )
344 25 recnd 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) e. CC )
345 18 67 344 68 fsumdivc 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) = sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) )
346 22 recnd 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( log ` x ) ^ k ) e. CC )
347 24 nnrpd 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. RR+ )
348 347 rpcnne0d 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ! ` k ) e. CC /\ ( ! ` k ) =/= 0 ) )
349 66 adantr 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( x e. CC /\ x =/= 0 ) )
350 divdiv32 
 |-  ( ( ( ( log ` x ) ^ k ) e. CC /\ ( ( ! ` k ) e. CC /\ ( ! ` k ) =/= 0 ) /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) = ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) )
351 346 348 349 350 syl3anc 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) = ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) )
352 351 sumeq2dv 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) = sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) )
353 345 352 eqtrd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) = sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) )
354 353 oveq2d 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ! ` N ) x. ( sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) / x ) ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) )
355 343 354 eqtrd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) )
356 355 mpteq2dva 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) = ( x e. RR+ |-> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ) )
357 2 adantr 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> x e. RR+ )
358 22 357 rerpdivcld 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` x ) ^ k ) / x ) e. RR )
359 358 24 nndivred 
 |-  ( ( ( N e. NN0 /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) e. RR )
360 18 359 fsumrecl 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) e. RR )
361 rpssre 
 |-  RR+ C_ RR
362 rlimconst 
 |-  ( ( RR+ C_ RR /\ ( ! ` N ) e. CC ) -> ( x e. RR+ |-> ( ! ` N ) ) ~~>r ( ! ` N ) )
363 361 34 362 sylancr 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ! ` N ) ) ~~>r ( ! ` N ) )
364 361 a1i 
 |-  ( N e. NN0 -> RR+ C_ RR )
365 fzfid 
 |-  ( N e. NN0 -> ( 0 ... N ) e. Fin )
366 359 anasss 
 |-  ( ( N e. NN0 /\ ( x e. RR+ /\ k e. ( 0 ... N ) ) ) -> ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) e. RR )
367 358 an32s 
 |-  ( ( ( N e. NN0 /\ k e. ( 0 ... N ) ) /\ x e. RR+ ) -> ( ( ( log ` x ) ^ k ) / x ) e. RR )
368 20 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> k e. NN0 )
369 368 faccld 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
370 369 nnred 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. RR )
371 370 adantr 
 |-  ( ( ( N e. NN0 /\ k e. ( 0 ... N ) ) /\ x e. RR+ ) -> ( ! ` k ) e. RR )
372 368 53 syl 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( x e. RR+ |-> ( ( ( log ` x ) ^ k ) / x ) ) ~~>r 0 )
373 369 nncnd 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. CC )
374 rlimconst 
 |-  ( ( RR+ C_ RR /\ ( ! ` k ) e. CC ) -> ( x e. RR+ |-> ( ! ` k ) ) ~~>r ( ! ` k ) )
375 361 373 374 sylancr 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( x e. RR+ |-> ( ! ` k ) ) ~~>r ( ! ` k ) )
376 369 nnne0d 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( ! ` k ) =/= 0 )
377 376 adantr 
 |-  ( ( ( N e. NN0 /\ k e. ( 0 ... N ) ) /\ x e. RR+ ) -> ( ! ` k ) =/= 0 )
378 367 371 372 375 376 377 rlimdiv 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ~~>r ( 0 / ( ! ` k ) ) )
379 373 376 div0d 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( 0 / ( ! ` k ) ) = 0 )
380 378 379 breqtrd 
 |-  ( ( N e. NN0 /\ k e. ( 0 ... N ) ) -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ~~>r 0 )
381 364 365 366 380 fsumrlim 
 |-  ( N e. NN0 -> ( x e. RR+ |-> sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ~~>r sum_ k e. ( 0 ... N ) 0 )
382 fzfi 
 |-  ( 0 ... N ) e. Fin
383 382 olci 
 |-  ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin )
384 sumz 
 |-  ( ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin ) -> sum_ k e. ( 0 ... N ) 0 = 0 )
385 383 384 ax-mp 
 |-  sum_ k e. ( 0 ... N ) 0 = 0
386 381 385 breqtrdi 
 |-  ( N e. NN0 -> ( x e. RR+ |-> sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ~~>r 0 )
387 17 360 363 386 rlimmul 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ) ~~>r ( ( ! ` N ) x. 0 ) )
388 34 mul01d 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. 0 ) = 0 )
389 387 388 breqtrd 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( ( log ` x ) ^ k ) / x ) / ( ! ` k ) ) ) ) ~~>r 0 )
390 356 389 eqbrtrd 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) ~~>r 0 )
391 56 341 54 390 rlimsub 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ N ) / x ) - ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) ) ~~>r ( 0 - 0 ) )
392 0m0e0 
 |-  ( 0 - 0 ) = 0
393 391 392 breqtrdi 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ N ) / x ) - ( ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) / x ) ) ) ~~>r 0 )
394 339 393 eqbrtrd 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) ~~>r 0 )
395 30 32 336 394 rlimadd 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) ) ~~>r ( ( ! ` N ) + 0 ) )
396 divsubdir 
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) e. CC /\ ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) - ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) )
397 58 63 66 396 syl3anc 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) - ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) )
398 397 oveq1d 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) - ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) )
399 10 2 rerpdivcld 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) e. RR )
400 399 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) e. CC )
401 32 recnd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) e. CC )
402 400 401 npcand 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) - ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) )
403 398 402 eqtrd 
 |-  ( ( N e. NN0 /\ x e. RR+ ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) )
404 403 mpteq2dva 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) - ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) ) / x ) + ( ( ( ( log ` x ) ^ N ) - ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( ( log ` x ) ^ k ) / ( ! ` k ) ) ) ) / x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) ) )
405 34 addridd 
 |-  ( N e. NN0 -> ( ( ! ` N ) + 0 ) = ( ! ` N ) )
406 395 404 405 3brtr3d 
 |-  ( N e. NN0 -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) ) ~~>r ( ! ` N ) )