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

Theorem logexprlim 20464
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 11035 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
2 simpr 447 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  RR+ )
3 elfznn 10819 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
43nnrpd 10389 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
5 rpdivcl 10376 . . . . . . . . 9  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
62, 4, 5syl2an 463 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
76relogcld 19974 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( log `  (
x  /  n ) )  e.  RR )
8 simpll 730 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  N  e.  NN0 )
97, 8reexpcld 11262 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n
) ) ^ N
)  e.  RR )
101, 9fsumrecl 12207 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  RR )
11 relogcl 19932 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
12 id 19 . . . . . . 7  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
13 reexpcl 11120 . . . . . . 7  |-  ( ( ( log `  x
)  e.  RR  /\  N  e.  NN0 )  -> 
( ( log `  x
) ^ N )  e.  RR )
1411, 12, 13syl2anr 464 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ N )  e.  RR )
15 faccl 11298 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
1615adantr 451 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  NN )
1716nnred 9761 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  RR )
18 fzfid 11035 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( 0 ... N
)  e.  Fin )
1911adantl 452 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( log `  x
)  e.  RR )
20 elfznn0 10822 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
21 reexpcl 11120 . . . . . . . . . 10  |-  ( ( ( log `  x
)  e.  RR  /\  k  e.  NN0 )  -> 
( ( log `  x
) ^ k )  e.  RR )
2219, 20, 21syl2an 463 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ( log `  x ) ^ k
)  e.  RR )
2320adantl 452 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  k  e.  NN0 )
24 faccl 11298 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
2523, 24syl 15 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ! `  k )  e.  NN )
2622, 25nndivred 9794 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  x  e.  RR+ )  /\  k  e.  (
0 ... N ) )  ->  ( ( ( log `  x ) ^ k )  / 
( ! `  k
) )  e.  RR )
2718, 26fsumrecl 12207 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  RR )
2817, 27remulcld 8863 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  RR )
2914, 28resubcld 9211 . . . . 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 9211 . . . 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 10417 . . 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 10381 . . . 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 648 . . 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 1re 8837 . . . . 5  |-  1  e.  RR
3534a1i 10 . . . 4  |-  ( N  e.  NN0  ->  1  e.  RR )
3615nncnd 9762 . . . 4  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  CC )
37 simpl 443 . . . . . . . . 9  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
k  =  N )
3837oveq2d 5874 . . . . . . . 8  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ k )  =  ( ( log `  x ) ^ N
) )
3938oveq1d 5873 . . . . . . 7  |-  ( ( k  =  N  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ k
)  /  x )  =  ( ( ( log `  x ) ^ N )  /  x ) )
4039mpteq2dva 4106 . . . . . 6  |-  ( k  =  N  ->  (
x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) )  =  ( x  e.  RR+  |->  ( ( ( log `  x ) ^ N )  /  x ) ) )
4140breq1d 4033 . . . . 5  |-  ( k  =  N  ->  (
( x  e.  RR+  |->  ( ( ( log `  x ) ^ k
)  /  x ) )  ~~> r  0  <->  (
x  e.  RR+  |->  ( ( ( log `  x
) ^ N )  /  x ) )  ~~> r  0 ) )
4211recnd 8861 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
43 id 19 . . . . . . . . 9  |-  ( k  e.  NN0  ->  k  e. 
NN0 )
44 cxpexp 20015 . . . . . . . . 9  |-  ( ( ( log `  x
)  e.  CC  /\  k  e.  NN0 )  -> 
( ( log `  x
)  ^ c  k )  =  ( ( log `  x ) ^ k ) )
4542, 43, 44syl2anr 464 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
)  ^ c  k )  =  ( ( log `  x ) ^ k ) )
46 rpcn 10362 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  CC )
4746adantl 452 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  CC )
4847cxp1d 20053 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( x  ^ c 
1 )  =  x )
4945, 48oveq12d 5876 . . . . . . 7  |-  ( ( k  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x )  ^ c 
k )  /  (
x  ^ c  1 ) )  =  ( ( ( log `  x
) ^ k )  /  x ) )
5049mpteq2dva 4106 . . . . . 6  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
)  ^ c  k )  /  ( x  ^ c  1 ) ) )  =  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) ) )
51 nn0cn 9975 . . . . . . 7  |-  ( k  e.  NN0  ->  k  e.  CC )
52 1rp 10358 . . . . . . 7  |-  1  e.  RR+
53 cxploglim2 20273 . . . . . . 7  |-  ( ( k  e.  CC  /\  1  e.  RR+ )  -> 
( x  e.  RR+  |->  ( ( ( log `  x )  ^ c 
k )  /  (
x  ^ c  1 ) ) )  ~~> r  0 )
5451, 52, 53sylancl 643 . . . . . 6  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
)  ^ c  k )  /  ( x  ^ c  1 ) ) )  ~~> r  0 )
5550, 54eqbrtrrd 4045 . . . . 5  |-  ( k  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ k )  /  x ) )  ~~> r  0 )
5641, 55vtoclga 2849 . . . 4  |-  ( N  e.  NN0  ->  ( x  e.  RR+  |->  ( ( ( log `  x
) ^ N )  /  x ) )  ~~> r  0 )
57 rerpdivcl 10381 . . . . . 6  |-  ( ( ( ( log `  x
) ^ N )  e.  RR  /\  x  e.  RR+ )  ->  (
( ( log `  x
) ^ N )  /  x )  e.  RR )
5814, 57sylancom 648 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  RR )
5958recnd 8861 . . . 4  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  CC )
6010recnd 8861 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  CC )
6114recnd 8861 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( log `  x
) ^ N )  e.  CC )
6236adantr 451 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ! `  N
)  e.  CC )
6327recnd 8861 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
6462, 63mulcld 8855 . . . . . . 7  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  CC )
6561, 64subcld 9157 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( ( ( log `  x ) ^ N
)  -  ( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  CC )
6660, 65subcld 9157 . . . . 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 )
67 rpcnne0 10371 . . . . . . 7  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
6867adantl 452 . . . . . 6  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  -> 
( x  e.  CC  /\  x  =/=  0 ) )
6968simpld 445 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  e.  CC )
7068simprd 449 . . . . 5  |-  ( ( N  e.  NN0  /\  x  e.  RR+ )  ->  x  =/=  0 )
7166, 69, 70divcld 9536 . . . 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 )
7271adantrr 697 . . . . . . . 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 )
7315adantr 451 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  e.  NN )
7473nncnd 9762 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  e.  CC )
7572, 74subcld 9157 . . . . . . 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 )
7675abscld 11918 . . . . . 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 )
7758adantrr 697 . . . . . 6  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  RR )
7877recnd 8861 . . . . . . 7  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( log `  x ) ^ N
)  /  x )  e.  CC )
7978abscld 11918 . . . . . 6  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( ( log `  x
) ^ N )  /  x ) )  e.  RR )
80 ioorp 10727 . . . . . . . . . 10  |-  ( 0 (,)  +oo )  =  RR+
8180eqcomi 2287 . . . . . . . . 9  |-  RR+  =  ( 0 (,)  +oo )
82 nnuz 10263 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
83 1z 10053 . . . . . . . . . 10  |-  1  e.  ZZ
8483a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ZZ )
8534a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  RR )
86 1nn0 9981 . . . . . . . . . . 11  |-  1  e.  NN0
8734, 86nn0addge1i 10012 . . . . . . . . . 10  |-  1  <_  ( 1  +  1 )
8887a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  ( 1  +  1 ) )
89 0re 8838 . . . . . . . . . 10  |-  0  e.  RR
9089a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  e.  RR )
9173adantr 451 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  NN )
9291nnred 9761 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  RR )
93 rpre 10360 . . . . . . . . . . . 12  |-  ( y  e.  RR+  ->  y  e.  RR )
9493adantl 452 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  y  e.  RR )
95 fzfid 11035 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( 0 ... N )  e. 
Fin )
96 simprl 732 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
97 rpdivcl 10376 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  y  e.  RR+ )  ->  (
x  /  y )  e.  RR+ )
9896, 97sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( x  /  y )  e.  RR+ )
9998relogcld 19974 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( log `  ( x  /  y
) )  e.  RR )
100 reexpcl 11120 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  y ) )  e.  RR  /\  k  e.  NN0 )  -> 
( ( log `  (
x  /  y ) ) ^ k )  e.  RR )
10199, 20, 100syl2an 463 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ( log `  ( x  /  y
) ) ^ k
)  e.  RR )
10220adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN0 )
103102, 24syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ! `  k )  e.  NN )
104101, 103nndivred 9794 . . . . . . . . . . . 12  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  e.  RR+ )  /\  k  e.  ( 0 ... N ) )  ->  ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  e.  RR )
10595, 104fsumrecl 12207 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  e.  RR )
10694, 105remulcld 8863 . . . . . . . . . 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 )
10792, 106remulcld 8863 . . . . . . . . 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 )
108 simpll 730 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  N  e.  NN0 )
10999, 108reexpcld 11262 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( log `  ( x  / 
y ) ) ^ N )  e.  RR )
110 nnrp 10363 . . . . . . . . . 10  |-  ( y  e.  NN  ->  y  e.  RR+ )
111110, 109sylan2 460 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  NN )  ->  ( ( log `  ( x  /  y ) ) ^ N )  e.  RR )
112 reex 8828 . . . . . . . . . . . . 13  |-  RR  e.  _V
113112prid1 3734 . . . . . . . . . . . 12  |-  RR  e.  { RR ,  CC }
114113a1i 10 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  RR  e.  { RR ,  CC } )
115106recnd 8861 . . . . . . . . . . 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 )
116109, 91nndivred 9794 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( (
( log `  (
x  /  y ) ) ^ N )  /  ( ! `  N ) )  e.  RR )
117 simpl 443 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  N  e.  NN0 )
118 advlogexp 20002 . . . . . . . . . . . 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 ) ) ) )
11996, 117, 118syl2anc 642 . . . . . . . . . . 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 ) ) ) )
120114, 115, 116, 119, 74dvmptcmul 19313 . . . . . . . . . 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 ) ) ) ) )
121109recnd 8861 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( log `  ( x  / 
y ) ) ^ N )  e.  CC )
12274adantr 451 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  e.  CC )
12373nnne0d 9790 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ! `  N
)  =/=  0 )
124123adantr 451 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ! `  N )  =/=  0
)
125121, 122, 124divcan2d 9538 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  ( ( ! `  N )  x.  ( ( ( log `  ( x  /  y
) ) ^ N
)  /  ( ! `
 N ) ) )  =  ( ( log `  ( x  /  y ) ) ^ N ) )
126125mpteq2dva 4106 . . . . . . . . . 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 ) ) )
127120, 126eqtrd 2315 . . . . . . . . 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
) ) )
128 oveq2 5866 . . . . . . . . . . 11  |-  ( y  =  n  ->  (
x  /  y )  =  ( x  /  n ) )
129128fveq2d 5529 . . . . . . . . . 10  |-  ( y  =  n  ->  ( log `  ( x  / 
y ) )  =  ( log `  (
x  /  n ) ) )
130129oveq1d 5873 . . . . . . . . 9  |-  ( y  =  n  ->  (
( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  ( x  /  n
) ) ^ N
) )
13196rpxrd 10391 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR* )
132 simp1rl 1020 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  x  e.  RR+ )
133 simp2r 982 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  e.  RR+ )
134132, 133rpdivcld 10407 . . . . . . . . . . 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+ )
135134relogcld 19974 . . . . . . . . . 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 )
136 simp2l 981 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
y  e.  RR+ )
137132, 136rpdivcld 10407 . . . . . . . . . . 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+ )
138137relogcld 19974 . . . . . . . . . 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 )
139 simp1l 979 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  N  e.  NN0 )
140 log1 19939 . . . . . . . . . . 11  |-  ( log `  1 )  =  0
141133rpcnd 10392 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  e.  CC )
142141mulid2d 8853 . . . . . . . . . . . . . 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 )
143 simp33 993 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  n  <_  x )
144142, 143eqbrtrd 4043 . . . . . . . . . . . . 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 )
14534a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
1  e.  RR )
146132rpred 10390 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  ->  x  e.  RR )
147145, 146, 133lemuldivd 10435 . . . . . . . . . . . . 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 ) ) )
148144, 147mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
1  <_  ( x  /  n ) )
149 logleb 19957 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
15052, 134, 149sylancr 644 . . . . . . . . . . . 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
) ) ) )
151148, 150mpbid 201 . . . . . . . . . . 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
) ) )
152140, 151syl5eqbrr 4057 . . . . . . . . . 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
) ) )
153 simp32 992 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  n  e.  RR+ )  /\  (
1  <_  y  /\  y  <_  n  /\  n  <_  x ) )  -> 
y  <_  n )
154136, 133, 132lediv2d 10414 . . . . . . . . . . . 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 ) ) )
155153, 154mpbid 201 . . . . . . . . . . 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 ) )
156134, 137logled 19978 . . . . . . . . . . 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
) ) ) )
157155, 156mpbid 201 . . . . . . . . . 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
) ) )
158 leexp1a 11160 . . . . . . . . . 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
) )
159135, 138, 139, 152, 157, 158syl32anc 1190 . . . . . . . . 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
) )
160 eqid 2283 . . . . . . . . 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
) ) ) ) ) )
161983ad2antr1 1120 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
x  /  y )  e.  RR+ )
162161relogcld 19974 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  ( log `  ( x  / 
y ) )  e.  RR )
163 simpll 730 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  N  e.  NN0 )
164 rpcn 10362 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR+  ->  y  e.  CC )
165164adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  e.  RR+ )  ->  y  e.  CC )
1661653ad2antr1 1120 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  e.  CC )
167166mulid2d 8853 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  x.  y )  =  y )
168 simpr3 963 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  <_  x )
169167, 168eqbrtrd 4043 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  x.  y )  <_  x )
17034a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  1  e.  RR )
17196rpred 10390 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
172171adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  x  e.  RR )
173 simpr1 961 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  y  e.  RR+ )
174170, 172, 173lemuldivd 10435 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
( 1  x.  y
)  <_  x  <->  1  <_  ( x  /  y ) ) )
175169, 174mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  1  <_  ( x  /  y
) )
176 logleb 19957 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR+  /\  (
x  /  y )  e.  RR+ )  ->  (
1  <_  ( x  /  y )  <->  ( log `  1 )  <_  ( log `  ( x  / 
y ) ) ) )
17752, 161, 176sylancr 644 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  (
1  <_  ( x  /  y )  <->  ( log `  1 )  <_  ( log `  ( x  / 
y ) ) ) )
178175, 177mpbid 201 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  ( log `  1 )  <_ 
( log `  (
x  /  y ) ) )
179140, 178syl5eqbrr 4057 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  0  <_  ( log `  (
x  /  y ) ) )
180162, 163, 179expge0d 11263 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  ( y  e.  RR+  /\  1  <_ 
y  /\  y  <_  x ) )  ->  0  <_  ( ( log `  (
x  /  y ) ) ^ N ) )
18152a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  RR+ )
182 1le1 9396 . . . . . . . . . 10  |-  1  <_  1
183182a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  1 )
184 simprr 733 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
185171leidd 9339 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  <_  x )
18681, 82, 84, 85, 88, 90, 107, 109, 111, 127, 130, 131, 159, 160, 180, 181, 96, 183, 184, 185dvfsumlem4 19376 . . . . . . . 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 ) )
187 fzfid 11035 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
18896, 4, 5syl2an 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
189188relogcld 19974 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
190 simpll 730 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN0 )
191189, 190reexpcld 11262 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^ N )  e.  RR )
192187, 191fsumrecl 12207 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  RR )
193192recnd 8861 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  e.  CC )
19496rpcnd 10392 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  CC )
19574, 194mulcld 8855 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ! `  N )  x.  x
)  e.  CC )
19611ad2antrl 708 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  RR )
197196recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  CC )
198197, 117expcld 11245 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
) ^ N )  e.  CC )
199 fzfid 11035 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 0 ... N
)  e.  Fin )
200196, 20, 21syl2an 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( log `  x
) ^ k )  e.  RR )
20120adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  k  e.  NN0 )
202201, 24syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  ( ! `  k )  e.  NN )
203200, 202nndivred 9794 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  RR )
204203recnd 8861 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  k  e.  ( 0 ... N
) )  ->  (
( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
205199, 204fsumcl 12206 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) )  e.  CC )
20674, 205mulcld 8855 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ! `  N )  x.  sum_ k  e.  ( 0 ... N ) ( ( ( log `  x
) ^ k )  /  ( ! `  k ) ) )  e.  CC )
207198, 206subcld 9157 . . . . . . . . . . . 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 )
208193, 195, 207sub32d 9189 . . . . . . . . . . 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 ) ) )
209 eqidd 2284 . . . . . . . . . . . . 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 ) ) ) ) ) ) )
210 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  y  =  x )
211210fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  ( |_ `  y )  =  ( |_ `  x
) )
212211oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... ( |_ `  x ) ) )
213212sumeq1d 12174 . . . . . . . . . . . . . 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 ) )
214 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  (
x  /  y )  =  ( x  /  x ) )
21567ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  e.  CC  /\  x  =/=  0 ) )
216 divid 9451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  CC  /\  x  =/=  0 )  -> 
( x  /  x
)  =  1 )
217215, 216syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  /  x
)  =  1 )
218214, 217sylan9eqr 2337 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
x  /  y )  =  1 )
219218adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( x  / 
y )  =  1 )
220219fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( log `  (
x  /  y ) )  =  ( log `  1 ) )
221220, 140syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( log `  (
x  /  y ) )  =  0 )
222221oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( ( log `  ( x  /  y
) ) ^ k
)  =  ( 0 ^ k ) )
223222oveq1d 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
0 ... N ) )  ->  ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  =  ( ( 0 ^ k
)  /  ( ! `
 k ) ) )
224223sumeq2dv 12176 . . . . . . . . . . . . . . . . . . 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 ) ) )
225 nn0uz 10262 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  =  ( ZZ>= `  0 )
226117, 225syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  N  e.  ( ZZ>= ` 
0 ) )
227 eluzfz1 10803 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
228226, 227syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  e.  ( 0 ... N ) )
229228adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  0  e.  ( 0 ... N
) )
230229snssd 3760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  { 0 }  C_  ( 0 ... N ) )
231 elsni 3664 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  { 0 }  ->  k  =  0 )
232231adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  k  =  0 )
233 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  0  ->  (
0 ^ k )  =  ( 0 ^ 0 ) )
234 0cn 8831 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  CC
235 exp0 11108 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  e.  CC  ->  (
0 ^ 0 )  =  1 )
236234, 235ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 ^ 0 )  =  1
237233, 236syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  0  ->  (
0 ^ k )  =  1 )
238 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  0  ->  ( ! `  k )  =  ( ! ` 
0 ) )
239 fac0 11291 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ! `
 0 )  =  1
240238, 239syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  0  ->  ( ! `  k )  =  1 )
241237, 240oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  0  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  ( 1  / 
1 ) )
242 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  CC
243242div1i 9488 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  /  1 )  =  1
244241, 243syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  0  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1 )
245232, 244syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1 )
246245, 242syl6eqel 2371 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  { 0 } )  ->  (
( 0 ^ k
)  /  ( ! `
 k ) )  e.  CC )
247 eldifi 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  ( ( 0 ... N )  \  { 0 } )  ->  k  e.  ( 0 ... N ) )
248247adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  ( 0 ... N ) )
249248, 20syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  NN0 )
250 eldifsni 3750 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( ( 0 ... N )  \  { 0 } )  ->  k  =/=  0
)
251250adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  =/=  0 )
252 eldifsn 3749 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( NN0  \  {
0 } )  <->  ( k  e.  NN0  /\  k  =/=  0 ) )
253249, 251, 252sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  ( NN0  \  { 0 } ) )
254 dfn2 9978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN  =  ( NN0  \  { 0 } )
255253, 254syl6eleqr 2374 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
k  e.  NN )
2562550expd 11261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( 0 ^ k
)  =  0 )
257256oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ( 0 ^ k )  /  ( ! `  k )
)  =  ( 0  /  ( ! `  k ) ) )
258249, 24syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  e.  NN )
259258nncnd 9762 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  e.  CC )
260258nnne0d 9790 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ! `  k
)  =/=  0 )
261259, 260div0d 9535 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( 0  /  ( ! `  k )
)  =  0 )
262257, 261eqtrd 2315 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  x )  /\  k  e.  (
( 0 ... N
)  \  { 0 } ) )  -> 
( ( 0 ^ k )  /  ( ! `  k )
)  =  0 )
263 fzfid 11035 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
0 ... N )  e. 
Fin )
264230, 246, 262, 263fsumss 12198 . . . . . . . . . . . . . . . . . . 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 )
) )
265224, 264eqtr4d 2318 . . . . . . . . . . . . . . . . . 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
) ) )
266244sumsn 12213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  CC  /\  1  e.  CC )  -> 
sum_ k  e.  {
0 }  ( ( 0 ^ k )  /  ( ! `  k ) )  =  1 )
267234, 242, 266mp2an 653 . . . . . . . . . . . . . . . . . 18  |-  sum_ k  e.  { 0 }  (
( 0 ^ k
)  /  ( ! `
 k ) )  =  1
268265, 267syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) )  =  1 )
269210, 268oveq12d 5876 . . . . . . . . . . . . . . . 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 ) )
270194mulid1d 8852 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  x.  1 )  =  x )
271270adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
x  x.  1 )  =  x )
272269, 271eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  =  x )  ->  (
y  x.  sum_ k  e.  ( 0 ... N
) ( ( ( log `  ( x  /  y ) ) ^ k )  / 
( ! `  k
) ) )  =  x )
273272oveq2d 5874 . . . . . . . . . . . . . 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 ) )
274213, 273oveq12d 5876 . . . . . . . . . . . . 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 ) ) )
275 ovex 5883 . . . . . . . . . . . . . 14  |-  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ N )  -  ( ( ! `  N )  x.  x
) )  e.  _V
276275a1i 10 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ N )  -  ( ( ! `
 N )  x.  x ) )  e. 
_V )
277209, 274, 96, 276fvmptd 5606 . . . . . . . . . . . 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 ) ) )
278 simpr 447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  y  =  1 )
279278fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( |_ `  y )  =  ( |_ `  1
) )
280 flid 10939 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  ZZ  ->  ( |_ `  1 )  =  1 )
28183, 280ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( |_
`  1 )  =  1
282279, 281syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( |_ `  y )  =  1 )
283282oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... 1
) )
284283sumeq1d 12174 . . . . . . . . . . . . . . 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 ) )
285194div1d 9528 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  /  1
)  =  x )
286285adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  1 )  =  x )
287286fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( log `  ( x  / 
1 ) )  =  ( log `  x
) )
288287oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  1 ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
289198adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  x
) ^ N )  e.  CC )
290288, 289eqeltrd 2357 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  1 ) ) ^ N )  e.  CC )
291 oveq2 5866 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
x  /  n )  =  ( x  / 
1 ) )
292291fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  ( log `  ( x  /  n ) )  =  ( log `  (
x  /  1 ) ) )
293292oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  ( x  /  1
) ) ^ N
) )
294293fsum1 12214 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  ( ( log `  (
x  /  1 ) ) ^ N )  e.  CC )  ->  sum_ n  e.  ( 1 ... 1 ) ( ( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  ( x  /  1
) ) ^ N
) )
29583, 290, 294sylancr 644 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ n  e.  ( 1 ... 1
) ( ( log `  ( x  /  n
) ) ^ N
)  =  ( ( log `  ( x  /  1 ) ) ^ N ) )
296284, 295, 2883eqtrd 2319 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ n  e.  ( 1 ... ( |_ `  y ) ) ( ( log `  (
x  /  n ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
297278oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  y )  =  ( x  / 
1 ) )
298297, 286eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
x  /  y )  =  x )
299298fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  ( log `  ( x  / 
y ) )  =  ( log `  x
) )
300299adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( log `  ( x  /  y
) )  =  ( log `  x ) )
301300oveq1d 5873 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( log `  ( x  / 
y ) ) ^
k )  =  ( ( log `  x
) ^ k ) )
302301oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  y  =  1 )  /\  k  e.  ( 0 ... N ) )  ->  ( (
( log `  (
x  /  y ) ) ^ k )  /  ( ! `  k ) )  =  ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) )
303302sumeq2dv 12176 . . . . . . . . . . . . . . . . 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 ) ) )
304278, 303oveq12d 5876 . . . . . . . . . . . . . . . 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 ) ) ) )
305205adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  sum_ k  e.  ( 0 ... N
) ( ( ( log `  x ) ^ k )  / 
( ! `  k
) )  e.  CC )
306305mulid2d 8853 . . . . . . . . . . . . . . . 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 ) ) )
307304, 306eqtrd 2315 . . . . . . . . . . . . . . 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 ) ) )
308307oveq2d 5874 . . . . . . . . . . . . . 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
) ) ) )
309296, 308oveq12d 5876 . . . . . . . . . . . . 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 ) ) ) ) )
310 ovex 5883 . . . . . . . . . . . . . 14  |-  ( ( ( log `  x
) ^ N )  -  ( ( ! `
 N )  x. 
sum_ k  e.  ( 0 ... N ) ( ( ( log `  x ) ^ k
)  /  ( ! `
 k ) ) ) )  e.  _V
311310a1i 10 . . . . . . . . . . . . 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 )
312209, 309, 181, 311fvmptd 5606 . . . . . . . . . . . 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 ) ) ) ) )
313277, 312oveq12d 5876 . . . . . . . . . . 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 ) ) ) ) ) )
31472, 74, 194subdird 9236 . . . . . . . . . . . 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 ) ) )
31566adantrr 697 . . . . . . . . . . . . . 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 )
316215simprd 449 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  =/=  0 )
317315, 194, 316divcan1d 9537 . . . . . . . . . . . . 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 ) ) ) ) ) )
318317oveq1d 5873 . . . . . . . . . . . 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 ) ) )
319314, 318eqtrd 2315 . . . . . . . . . . 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 ) ) )
320208, 313, 3193eqtr4d 2325 . . . . . . . . . 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 ) )
321320fveq2d 5529 . . . . . . . . 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 ) ) )
32275, 194absmuld 11936 . . . . . . . . 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 ) ) )
323 rprege0 10368 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <_  x ) )
324323ad2antrl 708 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  e.  RR  /\  0  <_  x )
)
325 absid 11781 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( abs `  x
)  =  x )
326324, 325syl 15 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  x
)  =  x )
327326oveq2d 5874 . . . . . . . . 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 ) )
328321, 322, 3273eqtrd 2319 . . . . . . . 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
) )
329242a1i 10 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  CC )
330299oveq1d 5873 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x )
)  /\  y  = 
1 )  ->  (
( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
331329, 330csbied 3123 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  [_ 1  /  y ]_ ( ( log `  (
x  /  y ) ) ^ N )  =  ( ( log `  x ) ^ N
) )
332186, 328, 3313brtr3d 4052 . . . . . . 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
) )
33314adantrr 697 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
) ^ N )  e.  RR )
33476, 333, 96lemuldivd 10435 . . . . . . 7  |-  ( ( N  e.