MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  logexprlim Structured version   Unicode version

Theorem logexprlim 22544
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.)
Assertion
Ref Expression
logexprlim  |-  ( N  e.  NN0  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ N )  /  x ) )  ~~> r  ( ! `  N ) )
Distinct variable group:    x, n, N

Proof of Theorem logexprlim
Dummy variables  k 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 11787 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
2 simpr 461 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  RR+ )
3 elfznn 11470 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
43nnrpd 11018 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
5 rpdivcl 11005 . . . . . . . . 9  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
62, 4, 5syl2an 477 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
76relogcld 22052 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( log `  (
x  /  n ) )  e.  RR )
8 simpll 753 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  N  e.  NN0 )
97, 8reexpcld 12017 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n
) ) ^ N
)  e.  RR )
101, 9fsumrecl 13203 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  RR )
11 relogcl 22007 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
12 id 22 . . . . . . 7  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
13 reexpcl 11874 . . . . . . 7  |-  ( ( ( log `  x
)  e.  RR  /\  N  e.  NN0 )  -> 
( ( log `  x
) ^ N )  e.  RR )
1411, 12, 13syl2anr 478 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ N )  e.  RR )
15 faccl 12053 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
1615adantr 465 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  NN )
1716nnred 10329 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  RR )
18 fzfid 11787 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( 0 ... N
)  e.  Fin )
1911adantl 466 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( log `  x
)  e.  RR )
20 elfznn0 11473 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
21 reexpcl 11874 . . . . . . . . . 10  |-  ( ( ( log `  x
)  e.  RR  /\  k  e.  NN0 )  -> 
( ( log `  x
) ^ k )  e.  RR )
2219, 20, 21syl2an 477 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ( log `  x ) ^ k
)  e.  RR )
2320adantl 466 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  k  e.  NN0 )
24 faccl 12053 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
2523, 24syl 16 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ! `  k )  e.  NN )
2622, 25nndivred 10362 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ( ( log `  x ) ^ k )  / 
( ! `  k
) )  e.  RR )
2718, 26fsumrecl 13203 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  RR )
2817, 27remulcld 9406 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  RR )
2914, 28resubcld 9768 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  RR )
3010, 29resubcld 9768 . . . 4  |-  ( ( 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 )
3130, 2rerpdivcld 11046 . . 3  |-  ( ( 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 )
32 rerpdivcl 11010 . . . 4  |-  ( ( ( ( ( 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 )
3329, 32sylancom 667 . . 3  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( ( log `  x ) ^ N )  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) ) )  /  x )  e.  RR )
34 1red 9393 . . . 4  |-  ( N  e.  NN0  ->  1  e.  RR )
3515nncnd 10330 . . . 4  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  CC )
36 simpl 457 . . . . . . . . 9  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
k  =  N )
3736oveq2d 6102 . . . . . . . 8  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ k )  =  ( ( log `  x ) ^ N
) )
3837oveq1d 6101 . . . . . . 7  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ k
)  /  x )  =  ( ( ( log `  x ) ^ N )  /  x ) )
3938mpteq2dva 4373 . . . . . 6  |-  ( k  =  N  ->  (
x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) )  =  ( x  e.  RR+  |->  ( ( ( log `  x ) ^ N )  /  x ) ) )
4039breq1d 4297 . . . . 5  |-  ( k  =  N  ->  (
( x  e.  RR+  |->  ( ( ( log `  x ) ^ k
)  /  x ) )  ~~> r  0  <->  (
x  e.  RR+  |->  ( ( ( log `  x
) ^ N )  /  x ) )  ~~> r  0 ) )
4111recnd 9404 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
42 id 22 . . . . . . . . 9  |-  ( k  e.  NN0  ->  k  e. 
NN0 )
43 cxpexp 22093 . . . . . . . . 9  |-  ( ( ( log `  x
)  e.  CC  /\  k  e.  NN0 )  -> 
( ( log `  x
)  ^c  k )  =  ( ( log `  x ) ^ k ) )
4441, 42, 43syl2anr 478 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
)  ^c  k )  =  ( ( log `  x ) ^ k ) )
45 rpcn 10991 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  CC )
4645adantl 466 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  CC )
4746cxp1d 22131 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( x  ^c 
1 )  =  x )
4844, 47oveq12d 6104 . . . . . . 7  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x )  ^c 
k )  /  (
x  ^c  1 ) )  =  ( ( ( log `  x
) ^ k )  /  x ) )
4948mpteq2dva 4373 . . . . . 6  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
)  ^c  k )  /  ( x  ^c  1 ) ) )  =  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) ) )
50 nn0cn 10581 . . . . . . 7  |-  ( k  e.  NN0  ->  k  e.  CC )
51 1rp 10987 . . . . . . 7  |-  1  e.  RR+
52 cxploglim2 22352 . . . . . . 7  |-  ( ( k  e.  CC  /\  1  e.  RR+ )  -> 
( x  e.  RR+  |->  ( ( ( log `  x )  ^c 
k )  /  (
x  ^c  1 ) ) )  ~~> r  0 )
5350, 51, 52sylancl 662 . . . . . 6  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
)  ^c  k )  /  ( x  ^c  1 ) ) )  ~~> r  0 )
5449, 53eqbrtrrd 4309 . . . . 5  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) )  ~~> r  0 )
5540, 54vtoclga 3031 . . . 4  |-  ( N  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ N )  /  x ) )  ~~> r  0 )
56 rerpdivcl 11010 . . . . . 6  |-  ( ( ( ( log `  x
) ^ N )  e.  RR  /\  x  e.  RR+ )  ->  (
( ( log `  x
) ^ N )  /  x )  e.  RR )
5714, 56sylancom 667 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  RR )
5857recnd 9404 . . . 4  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  CC )
5910recnd 9404 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  CC )
6014recnd 9404 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ N )  e.  CC )
6135adantr 465 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  CC )
6227recnd 9404 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
6361, 62mulcld 9398 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  CC )
6460, 63subcld 9711 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  CC )
6559, 64subcld 9711 . . . . 5  |-  ( ( 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 )
66 rpcnne0 11000 . . . . . . 7  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
6766adantl 466 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( x  e.  CC  /\  x  =/=  0 ) )
6867simpld 459 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  CC )
6967simprd 463 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  =/=  0 )
7065, 68, 69divcld 10099 . . . 4  |-  ( ( 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 )
7170adantrr 716 . . . . . . . 8  |-  ( ( 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 )
7215adantr 465 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  e.  NN )
7372nncnd 10330 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  e.  CC )
7471, 73subcld 9711 . . . . . . 7  |-  ( ( 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 )
7574abscld 12914 . . . . . 6  |-  ( ( 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 )
7657adantrr 716 . . . . . 6  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  RR )
7776recnd 9404 . . . . . . 7  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  CC )
7877abscld 12914 . . . . . 6  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( ( log `  x
) ^ N )  /  x ) )  e.  RR )
79 ioorp 11365 . . . . . . . . . 10  |-  ( 0 (,) +oo )  = 
RR+
8079eqcomi 2442 . . . . . . . . 9  |-  RR+  =  ( 0 (,) +oo )
81 nnuz 10888 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
82 1z 10668 . . . . . . . . . 10  |-  1  e.  ZZ
8382a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ZZ )
84 1red 9393 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  RR )
85 1re 9377 . . . . . . . . . . 11  |-  1  e.  RR
86 1nn0 10587 . . . . . . . . . . 11  |-  1  e.  NN0
8785, 86nn0addge1i 10620 . . . . . . . . . 10  |-  1  <_  ( 1  +  1 )
8887a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  ( 1  +  1 ) )
89 0red 9379 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  e.  RR )
9072adantr 465 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  NN )
9190nnred 10329 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  RR )
92 rpre 10989 . . . . . . . . . . . 12  |-  ( y  e.  RR+  ->  y  e.  RR )
9392adantl 466 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  y  e.  RR )
94 fzfid 11787 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( 0 ... N )  e. 
Fin )
95 simprl 755 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
96 rpdivcl 11005 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  y  e.  RR+ )  ->  (
x  /  y )  e.  RR+ )
9795, 96sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( x  /  y )  e.  RR+ )
9897relogcld 22052 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( log `  ( x  /  y
) )  e.  RR )
99 reexpcl 11874 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  y ) )  e.  RR  /\  k  e.  NN0 )  -> 
( ( log `  (
x  /  y ) ) ^ k )  e.  RR )
10098, 20, 99syl2an 477 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ( log `  ( x  /  y
) ) ^ k
)  e.  RR )
10120adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN0 )
102101, 24syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ! `  k )  e.  NN )
103100, 102nndivred 10362 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  e.  RR )
10494, 103fsumrecl 13203 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  e.  RR )
10593, 104remulcld 9406 . . . . . . . . . 10  |-  ( ( ( 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 )
10691, 105remulcld 9406 . . . . . . . . 9  |-  ( ( ( 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 )
107 simpll 753 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  N  e.  NN0 )
10898, 107reexpcld 12017 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( log `  ( x  / 
y ) ) ^ N )  e.  RR )
109 nnrp 10992 . . . . . . . . . 10  |-  ( y  e.  NN  ->  y  e.  RR+ )
110109, 108sylan2 474 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  NN )  ->  ( ( log `  ( x  /  y ) ) ^ N )  e.  RR )
111 reelprrecn 9366 . . . . . . . . . . . 12  |-  RR  e.  { RR ,  CC }
112111a1i 11 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  RR  e.  { RR ,  CC } )
113105recnd 9404 . . . . . . . . . . 11  |-  ( ( ( 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 )
114108, 90nndivred 10362 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( (
( log `  (
x  /  y ) ) ^ N )  /  ( ! `  N ) )  e.  RR )
115 simpl 457 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  N  e.  NN0 )
116 advlogexp 22080 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) )
11795, 115, 116syl2anc 661 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
118112, 113, 114, 117, 73dvmptcmul 21418 . . . . . . . . . 10  |-  ( ( 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 ) ) ) ) )
119108recnd 9404 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( log `  ( x  / 
y ) ) ^ N )  e.  CC )
12073adantr 465 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  CC )
12172nnne0d 10358 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  =/=  0 )
122121adantr 465 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  =/=  0
)
123119, 120, 122divcan2d 10101 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( ! `  N )  x.  ( ( ( log `  ( x  /  y
) ) ^ N
)  /  ( ! `
 N ) ) )  =  ( ( log `  ( x  /  y ) ) ^ N ) )
124123mpteq2dva 4373 . . . . . . . . . 10  |-  ( ( 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 ) ) )
125118, 124eqtrd 2470 . . . . . . . . 9  |-  ( ( 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
) ) )
126 oveq2 6094 . . . . . . . . . . 11  |-  ( y  =  n  ->  (
x  /  y )  =  ( x  /  n ) )
127126fveq2d 5690 . . . . . . . . . 10  |-  ( y  =  n  ->  ( log `  ( x  / 
y ) )  =  ( log `  (
x  /  n ) ) )
128127oveq1d 6101 . . . . . . . . 9  |-  ( y  =  n  ->  (
( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  ( x  /  n
) ) ^ N
) )
12995rpxrd 11020 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR* )
130 simp1rl 1053 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  x  e.  RR+ )
131 simp2r 1015 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  e.  RR+ )
132130, 131rpdivcld 11036 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
( x  /  n
)  e.  RR+ )
133132relogcld 22052 . . . . . . . . . 10  |-  ( ( ( 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 )
134 simp2l 1014 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
y  e.  RR+ )
135130, 134rpdivcld 11036 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
( x  /  y
)  e.  RR+ )
136135relogcld 22052 . . . . . . . . . 10  |-  ( ( ( 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 )
137 simp1l 1012 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  N  e.  NN0 )
138 log1 22014 . . . . . . . . . . 11  |-  ( log `  1 )  =  0
139131rpcnd 11021 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  e.  CC )
140139mulid2d 9396 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
( 1  x.  n
)  =  n )
141 simp33 1026 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  <_  x )
142140, 141eqbrtrd 4307 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
( 1  x.  n
)  <_  x )
143 1red 9393 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
1  e.  RR )
144130rpred 11019 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  x  e.  RR )
145143, 144, 131lemuldivd 11064 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
146142, 145mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
1  <_  ( x  /  n ) )
147 logleb 22032 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
14851, 132, 147sylancr 663 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) )
149146, 148mpbid 210 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
150138, 149syl5eqbrr 4321 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
0  <_  ( log `  ( x  /  n
) ) )
151 simp32 1025 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
y  <_  n )
152134, 131, 130lediv2d 11043 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
153151, 152mpbid 210 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
( x  /  n
)  <_  ( x  /  y ) )
154132, 135logled 22056 . . . . . . . . . . 11  |-  ( ( ( 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
) ) ) )
155153, 154mpbid 210 . . . . . . . . . 10  |-  ( ( ( 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
) ) )
156 leexp1a 11914 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
157133, 136, 137, 150, 155, 156syl32anc 1226 . . . . . . . . 9  |-  ( ( ( 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
) )
158 eqid 2438 . . . . . . . . 9  |-  ( 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
) ) ) ) ) )
159973ad2antr1 1153 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
x  /  y )  e.  RR+ )
160159relogcld 22052 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  ( log `  ( x  / 
y ) )  e.  RR )
161 simpll 753 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  N  e.  NN0 )
162 rpcn 10991 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR+  ->  y  e.  CC )
163162adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  y  e.  CC )
1641633ad2antr1 1153 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  e.  CC )
165164mulid2d 9396 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  x.  y )  =  y )
166 simpr3 996 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  <_  x )
167165, 166eqbrtrd 4307 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  x.  y )  <_  x )
168 1red 9393 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  1  e.  RR )
16995rpred 11019 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
170169adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  x  e.  RR )
171 simpr1 994 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  e.  RR+ )
172168, 170, 171lemuldivd 11064 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
( 1  x.  y
)  <_  x  <->  1  <_  ( x  /  y ) ) )
173167, 172mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  1  <_  ( x  /  y
) )
174 logleb 22032 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR+  /\  (
x  /  y )  e.  RR+ )  ->  (
1  <_  ( x  /  y )  <->  ( log `  1 )  <_  ( log `  ( x  / 
y ) ) ) )
17551, 159, 174sylancr 663 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  <_  ( x  /  y )  <->  ( log `  1 )  <_  ( log `  ( x  / 
y ) ) ) )
176173, 175mpbid 210 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  ( log `  1 )  <_ 
( log `  (
x  /  y ) ) )
177138, 176syl5eqbrr 4321 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  0  <_  ( log `  (
x  /  y ) ) )
178160, 161, 177expge0d 12018 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  0  <_  ( ( log `  (
x  /  y ) ) ^ N ) )
17951a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  RR+ )
180 1le1 9956 . . . . . . . . . 10  |-  1  <_  1
181180a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  1 )
182 simprr 756 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
183169leidd 9898 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  <_  x )
18480, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183dvfsumlem4 21481 . . . . . . . 8  |-  ( ( 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 ) )
185 fzfid 11787 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
18695, 4, 5syl2an 477 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
187186relogcld 22052 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
188 simpll 753 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN0 )
189187, 188reexpcld 12017 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^ N )  e.  RR )
190185, 189fsumrecl 13203 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  RR )
191190recnd 9404 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  CC )
19295rpcnd 11021 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  CC )
19373, 192mulcld 9398 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ! `  N )  x.  x
)  e.  CC )
19411ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  RR )
195194recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  CC )
196195, 115expcld 12000 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
) ^ N )  e.  CC )
197 fzfid 11787 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 0 ... N
)  e.  Fin )
198194, 20, 21syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( log `  x
) ^ k )  e.  RR )
19920adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  k  e.  NN0 )
200199, 24syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  ( ! `  k )  e.  NN )
201198, 200nndivred 10362 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  RR )
202201recnd 9404 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
203197, 202fsumcl 13202 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
20473, 203mulcld 9398 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  CC )
205196, 204subcld 9711 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  CC )
206191, 193, 205sub32d 9743 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
207 eqidd 2439 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) ) ) )
208 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  y  =  x )
209208fveq2d 5690 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  ( |_ `  y )  =  ( |_ `  x
) )
210209oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... ( |_ `  x ) ) )
211210sumeq1d 13170 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
212 oveq2 6094 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  (
x  /  y )  =  ( x  /  x ) )
21366ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  e.  CC  /\  x  =/=  0 ) )
214 divid 10013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  CC  /\  x  =/=  0 )  -> 
( x  /  x
)  =  1 )
215213, 214syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  /  x
)  =  1 )
216212, 215sylan9eqr 2492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
x  /  y )  =  1 )
217216adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( x  / 
y )  =  1 )
218217fveq2d 5690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( log `  (
x  /  y ) )  =  ( log `  1 ) )
219218, 138syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( log `  (
x  /  y ) )  =  0 )
220219oveq1d 6101 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( ( log `  ( x  /  y
) ) ^ k
)  =  ( 0 ^ k ) )
221220oveq1d 6101 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  =  ( ( 0 ^ k
)  /  ( ! `
 k ) ) )
222221sumeq2dv 13172 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
223 nn0uz 10887 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  =  ( ZZ>= `  0 )
224115, 223syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  N  e.  ( ZZ>= ` 
0 ) )
225 eluzfz1 11450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
226224, 225syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  e.  ( 0 ... N ) )
227226adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  0  e.  ( 0 ... N
) )
228227snssd 4013 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  { 0 }  C_  ( 0 ... N ) )
229 elsni 3897 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  { 0 }  ->  k  =  0 )
230229adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  k  =  0 )
231 oveq2 6094 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  0  ->  (
0 ^ k )  =  ( 0 ^ 0 ) )
232 0exp0e1 11862 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 ^ 0 )  =  1
233231, 232syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  0  ->  (
0 ^ k )  =  1 )
234 fveq2 5686 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  0  ->  ( ! `  k )  =  ( ! ` 
0 ) )
235 fac0 12046 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ! `
 0 )  =  1
236234, 235syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  0  ->  ( ! `  k )  =  1 )
237233, 236oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  0  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  ( 1  / 
1 ) )
238 1div1e1 10016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  /  1 )  =  1
239237, 238syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  0  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1 )
240230, 239syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1 )
241 ax-1cn 9332 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
242240, 241syl6eqel 2526 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  e.  CC )
243 eldifi 3473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  ( ( 0 ... N )  \  { 0 } )  ->  k  e.  ( 0 ... N ) )
244243adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  ( 0 ... N ) )
245244, 20syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  NN0 )
246 eldifsni 3996 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( ( 0 ... N )  \  { 0 } )  ->  k  =/=  0
)
247246adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  =/=  0 )
248 eldifsn 3995 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( NN0  \  {
0 } )  <->  ( k  e.  NN0  /\  k  =/=  0 ) )
249245, 247, 248sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  ( NN0  \  { 0 } ) )
250 dfn2 10584 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN  =  ( NN0  \  { 0 } )
251249, 250syl6eleqr 2529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  NN )
2522510expd 12016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( 0 ^ k
)  =  0 )
253252oveq1d 6101 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ( 0 ^ k )  /  ( ! `  k )
)  =  ( 0  /  ( ! `  k ) ) )
254245, 24syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  e.  NN )
255254nncnd 10330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  e.  CC )
256254nnne0d 10358 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  =/=  0 )
257255, 256div0d 10098 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( 0  /  ( ! `  k )
)  =  0 )
258253, 257eqtrd 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ( 0 ^ k )  /  ( ! `  k )
)  =  0 )
259 fzfid 11787 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
0 ... N )  e. 
Fin )
260228, 242, 258, 259fsumss 13194 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 )
) )
261222, 260eqtr4d 2473 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )
262 0cn 9370 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  CC
263239sumsn 13209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  CC  /\  1  e.  CC )  -> 
sum_ k  e.  {
0 }  ( ( 0 ^ k )  /  ( ! `  k ) )  =  1 )
264262, 241, 263mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  sum_ k  e.  { 0 }  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1
265261, 264syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  =  1 )
266208, 265oveq12d 6104 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
267192mulid1d 9395 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  x.  1 )  =  x )
268267adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
x  x.  1 )  =  x )
269266, 268eqtrd 2470 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
y  x.  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) ) )  =  x )
270269oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
271211, 270oveq12d 6104 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
272 ovex 6111 . . . . . . . . . . . . . 14  |-  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ N )  -  ( ( ! `  N )  x.  x
) )  e.  _V
273272a1i 11 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  -  ( ( ! `
 N )  x.  x ) )  e. 
_V )
274207, 271, 95, 273fvmptd 5774 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
275 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  y  =  1 )
276275fveq2d 5690 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( |_ `  y )  =  ( |_ `  1
) )
277 flid 11649 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  ZZ  ->  ( |_ `  1 )  =  1 )
27882, 277ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( |_
`  1 )  =  1
279276, 278syl6eq 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( |_ `  y )  =  1 )
280279oveq2d 6102 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... 1
) )
281280sumeq1d 13170 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
282192div1d 10091 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  /  1
)  =  x )
283282adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  1 )  =  x )
284283fveq2d 5690 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( log `  ( x  / 
1 ) )  =  ( log `  x
) )
285284oveq1d 6101 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  1 ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
286196adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  x
) ^ N )  e.  CC )
287285, 286eqeltrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  1 ) ) ^ N )  e.  CC )
288 oveq2 6094 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
x  /  n )  =  ( x  / 
1 ) )
289288fveq2d 5690 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  ( log `  ( x  /  n ) )  =  ( log `  (
x  /  1 ) ) )
290289oveq1d 6101 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  ( x  /  1
) ) ^ N
) )
291290fsum1 13210 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  ( ( log `  (
x  /  1 ) ) ^ N )  e.  CC )  ->  sum_ n  e.  ( 1 ... 1 ) ( ( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  ( x  /  1
) ) ^ N
) )
29282, 287, 291sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ n  e.  ( 1 ... 1
) ( ( log `  ( x  /  n
) ) ^ N
)  =  ( ( log `  ( x  /  1 ) ) ^ N ) )
293281, 292, 2853eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ n  e.  ( 1 ... ( |_ `  y ) ) ( ( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
294275oveq2d 6102 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  y )  =  ( x  / 
1 ) )
295294, 283eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  y )  =  x )
296295fveq2d 5690 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( log `  ( x  / 
y ) )  =  ( log `  x
) )
297296adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( log `  ( x  /  y
) )  =  ( log `  x ) )
298297oveq1d 6101 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( log `  ( x  / 
y ) ) ^
k )  =  ( ( log `  x
) ^ k ) )
299298oveq1d 6101 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( (
( log `  (
x  /  y ) ) ^ k )  /  ( ! `  k ) )  =  ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) )
300299sumeq2dv 13172 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
301275, 300oveq12d 6104 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
302203adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  x ) ^ k )  / 
( ! `  k
) )  e.  CC )
303302mulid2d 9396 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
304301, 303eqtrd 2470 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
305304oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
306293, 305oveq12d 6104 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) )
307 ovex 6111 . . . . . . . . . . . . . 14  |-  ( ( ( log `  x
) ^ N )  -  ( ( ! `
 N )  x. 
sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  _V
308307a1i 11 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  _V )
309207, 306, 179, 308fvmptd 5774 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) )
310274, 309oveq12d 6104 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) ) )
31171, 73, 192subdird 9793 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
31265adantrr 716 . . . . . . . . . . . . . 14  |-  ( ( 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 )
313213simprd 463 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  =/=  0 )
314312, 192, 313divcan1d 10100 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) ) )
315314oveq1d 6101 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
316311, 315eqtrd 2470 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
317206, 310, 3163eqtr4d 2480 . . . . . . . . . 10  |-  ( ( 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 ) )
318317fveq2d 5690 . . . . . . . . 9  |-  ( ( 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 ) ) )
31974, 192absmuld 12932 . . . . . . . . 9  |-  ( ( 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 ) ) )
320 rprege0 10997 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <_  x ) )
321320ad2antrl 727 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  e.  RR  /\  0  <_  x )
)
322 absid 12777 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( abs `  x
)  =  x )
323321, 322syl 16 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  x
)  =  x )
324323oveq2d 6102 . . . . . . . . 9  |-  ( ( 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 ) )
325318, 319, 3243eqtrd 2474 . . . . . . . 8  |-  ( ( 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
) )
326 1cnd 9394 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  CC )
327296oveq1d 6101 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
328326, 327csbied 3309 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  [_ 1  /  y ]_ ( ( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
329184, 325, 3283brtr3d 4316 . . . . . . 7  |-  ( ( 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
) )
33014adantrr 716 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
) ^ N )  e.  RR )
33175, 330, 95lemuldivd 11064 . . . . . . 7  |-  ( ( 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 `