Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem4 Unicode version

Theorem stirlinglem4 27929
Description: Algebraic manipulation of  ( ( B n ) - ( B  ( n  +  1 ) ) ). It will be used in other theorems to show that  B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem4.1  |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
( sqr `  (
2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )
stirlinglem4.2  |-  B  =  ( n  e.  NN  |->  ( log `  ( A `
 n ) ) )
stirlinglem4.3  |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  ( 2  x.  n ) )  /  2 )  x.  ( log `  (
( n  +  1 )  /  n ) ) )  -  1 ) )
Assertion
Ref Expression
stirlinglem4  |-  ( N  e.  NN  ->  (
( B `  N
)  -  ( B `
 ( N  + 
1 ) ) )  =  ( J `  N ) )
Distinct variable group:    n, N
Allowed substitution hints:    A( n)    B( n)    J( n)

Proof of Theorem stirlinglem4
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 stirlinglem4.1 . . . . . . . 8  |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
( sqr `  (
2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )
21stirlinglem2 27927 . . . . . . 7  |-  ( N  e.  NN  ->  ( A `  N )  e.  RR+ )
32relogcld 19990 . . . . . 6  |-  ( N  e.  NN  ->  ( log `  ( A `  N ) )  e.  RR )
43ancli 534 . . . . 5  |-  ( N  e.  NN  ->  ( N  e.  NN  /\  ( log `  ( A `  N ) )  e.  RR ) )
5 id 19 . . . . . 6  |-  ( ( N  e.  NN  /\  ( log `  ( A `
 N ) )  e.  RR )  -> 
( N  e.  NN  /\  ( log `  ( A `  N )
)  e.  RR ) )
6 nfcv 2432 . . . . . . 7  |-  F/_ n N
7 nfcv 2432 . . . . . . . 8  |-  F/_ n log
8 nfmpt1 4125 . . . . . . . . . 10  |-  F/_ n
( n  e.  NN  |->  ( ( ! `  n )  /  (
( sqr `  (
2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )
91, 8nfcxfr 2429 . . . . . . . . 9  |-  F/_ n A
109, 6nffv 5548 . . . . . . . 8  |-  F/_ n
( A `  N
)
117, 10nffv 5548 . . . . . . 7  |-  F/_ n
( log `  ( A `  N )
)
12 fveq2 5541 . . . . . . . 8  |-  ( n  =  N  ->  ( A `  n )  =  ( A `  N ) )
1312fveq2d 5545 . . . . . . 7  |-  ( n  =  N  ->  ( log `  ( A `  n ) )  =  ( log `  ( A `  N )
) )
14 stirlinglem4.2 . . . . . . 7  |-  B  =  ( n  e.  NN  |->  ( log `  ( A `
 n ) ) )
156, 11, 13, 14fvmptf 5632 . . . . . 6  |-  ( ( N  e.  NN  /\  ( log `  ( A `
 N ) )  e.  RR )  -> 
( B `  N
)  =  ( log `  ( A `  N
) ) )
165, 15syl 15 . . . . 5  |-  ( ( N  e.  NN  /\  ( log `  ( A `
 N ) )  e.  RR )  -> 
( B `  N
)  =  ( log `  ( A `  N
) ) )
174, 16syl 15 . . . 4  |-  ( N  e.  NN  ->  ( B `  N )  =  ( log `  ( A `  N )
) )
18 nfcv 2432 . . . . . . . 8  |-  F/_ k
( log `  ( A `  n )
)
19 nfcv 2432 . . . . . . . . . 10  |-  F/_ n
k
209, 19nffv 5548 . . . . . . . . 9  |-  F/_ n
( A `  k
)
217, 20nffv 5548 . . . . . . . 8  |-  F/_ n
( log `  ( A `  k )
)
22 fveq2 5541 . . . . . . . . 9  |-  ( n  =  k  ->  ( A `  n )  =  ( A `  k ) )
2322fveq2d 5545 . . . . . . . 8  |-  ( n  =  k  ->  ( log `  ( A `  n ) )  =  ( log `  ( A `  k )
) )
2418, 21, 23cbvmpt 4126 . . . . . . 7  |-  ( n  e.  NN  |->  ( log `  ( A `  n
) ) )  =  ( k  e.  NN  |->  ( log `  ( A `
 k ) ) )
2514, 24eqtri 2316 . . . . . 6  |-  B  =  ( k  e.  NN  |->  ( log `  ( A `
 k ) ) )
2625a1i 10 . . . . 5  |-  ( N  e.  NN  ->  B  =  ( k  e.  NN  |->  ( log `  ( A `  k )
) ) )
27 simpr 447 . . . . . . 7  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  k  =  ( N  +  1 ) )
2827fveq2d 5545 . . . . . 6  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( A `  k )  =  ( A `  ( N  +  1 ) ) )
2928fveq2d 5545 . . . . 5  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( log `  ( A `  k )
)  =  ( log `  ( A `  ( N  +  1 ) ) ) )
30 peano2nn 9774 . . . . 5  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  NN )
311stirlinglem2 27927 . . . . . . 7  |-  ( ( N  +  1 )  e.  NN  ->  ( A `  ( N  +  1 ) )  e.  RR+ )
3230, 31syl 15 . . . . . 6  |-  ( N  e.  NN  ->  ( A `  ( N  +  1 ) )  e.  RR+ )
3332relogcld 19990 . . . . 5  |-  ( N  e.  NN  ->  ( log `  ( A `  ( N  +  1
) ) )  e.  RR )
3426, 29, 30, 33fvmptd 5622 . . . 4  |-  ( N  e.  NN  ->  ( B `  ( N  +  1 ) )  =  ( log `  ( A `  ( N  +  1 ) ) ) )
3517, 34oveq12d 5892 . . 3  |-  ( N  e.  NN  ->  (
( B `  N
)  -  ( B `
 ( N  + 
1 ) ) )  =  ( ( log `  ( A `  N
) )  -  ( log `  ( A `  ( N  +  1
) ) ) ) )
362, 32relogdivd 19993 . . . 4  |-  ( N  e.  NN  ->  ( log `  ( ( A `
 N )  / 
( A `  ( N  +  1 ) ) ) )  =  ( ( log `  ( A `  N )
)  -  ( log `  ( A `  ( N  +  1 ) ) ) ) )
3736eqcomd 2301 . . 3  |-  ( N  e.  NN  ->  (
( log `  ( A `  N )
)  -  ( log `  ( A `  ( N  +  1 ) ) ) )  =  ( log `  (
( A `  N
)  /  ( A `
 ( N  + 
1 ) ) ) ) )
38 id 19 . . . . . . . 8  |-  ( N  e.  NN  ->  N  e.  NN )
39 nnnn0 9988 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  NN0 )
40 faccl 11314 . . . . . . . . . 10  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
41 nnrp 10379 . . . . . . . . . 10  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  RR+ )
4239, 40, 413syl 18 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( ! `  N )  e.  RR+ )
43 2rp 10375 . . . . . . . . . . . . 13  |-  2  e.  RR+
4443a1i 10 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  2  e.  RR+ )
45 nnrp 10379 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  RR+ )
4644, 45rpmulcld 10422 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
2  x.  N )  e.  RR+ )
4746rpsqrcld 11910 . . . . . . . . . 10  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  N ) )  e.  RR+ )
48 epr 12502 . . . . . . . . . . . . 13  |-  _e  e.  RR+
4948a1i 10 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  _e  e.  RR+ )
5045, 49rpdivcld 10423 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( N  /  _e )  e.  RR+ )
51 nnz 10061 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  N  e.  ZZ )
5250, 51rpexpcld 11284 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( N  /  _e ) ^ N )  e.  RR+ )
5347, 52rpmulcld 10422 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) )  e.  RR+ )
5442, 53rpdivcld 10423 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ! `  N
)  /  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )
5538, 54jca 518 . . . . . . 7  |-  ( N  e.  NN  ->  ( N  e.  NN  /\  (
( ! `  N
)  /  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ ) )
561a1i 10 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  ( ( sqr `  ( 2  x.  n
) )  x.  (
( n  /  _e ) ^ n ) ) ) ) )
57 simpr 447 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  n  =  N )
5857fveq2d 5545 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( ! `  n )  =  ( ! `  N ) )
5957oveq2d 5890 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( 2  x.  n )  =  ( 2  x.  N
) )
6059fveq2d 5545 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( sqr `  ( 2  x.  n
) )  =  ( sqr `  ( 2  x.  N ) ) )
6157oveq1d 5889 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( n  /  _e )  =  ( N  /  _e ) )
6261, 57oveq12d 5892 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( (
n  /  _e ) ^ n )  =  ( ( N  /  _e ) ^ N ) )
6360, 62oveq12d 5892 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) )  =  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )
6458, 63oveq12d 5892 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  /\  n  =  N
)  ->  ( ( ! `  n )  /  ( ( sqr `  ( 2  x.  n
) )  x.  (
( n  /  _e ) ^ n ) ) )  =  ( ( ! `  N )  /  ( ( sqr `  ( 2  x.  N
) )  x.  (
( N  /  _e ) ^ N ) ) ) )
65 simpl 443 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  N  e.  NN )
6642rpcnd 10408 . . . . . . . . . 10  |-  ( N  e.  NN  ->  ( ! `  N )  e.  CC )
6766adantr 451 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ! `  N
)  e.  CC )
68 2cn 9832 . . . . . . . . . . . . 13  |-  2  e.  CC
6968a1i 10 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  2  e.  CC )
7065nncnd 9778 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  N  e.  CC )
7169, 70mulcld 8871 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( 2  x.  N
)  e.  CC )
7271sqrcld 11935 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( sqr `  (
2  x.  N ) )  e.  CC )
73 ere 12386 . . . . . . . . . . . . . 14  |-  _e  e.  RR
7473recni 8865 . . . . . . . . . . . . 13  |-  _e  e.  CC
7574a1i 10 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  _e  e.  CC )
76 0re 8854 . . . . . . . . . . . . . . 15  |-  0  e.  RR
77 epos 12501 . . . . . . . . . . . . . . 15  |-  0  <  _e
7876, 77pm3.2i 441 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  /\  0  <  _e )
79 ltne 8933 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  0  <  _e )  ->  _e  =/=  0 )
8078, 79ax-mp 8 . . . . . . . . . . . . 13  |-  _e  =/=  0
8180a1i 10 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  _e  =/=  0 )
8270, 75, 81divcld 9552 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( N  /  _e )  e.  CC )
8365, 39syl 15 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  N  e.  NN0 )
8482, 83expcld 11261 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ( N  /  _e ) ^ N )  e.  CC )
8572, 84mulcld 8871 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) )  e.  CC )
8676a1i 10 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  0  e.  RR )
8747rpgt0d 10409 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  0  <  ( sqr `  (
2  x.  N ) ) )
8886, 87gtned 8970 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  N ) )  =/=  0 )
8965, 88syl 15 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( sqr `  (
2  x.  N ) )  =/=  0 )
9065nnne0d 9806 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  N  =/=  0 )
9170, 75, 90, 81divne0d 9568 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( N  /  _e )  =/=  0 )
9265, 51syl 15 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  N  e.  ZZ )
9382, 91, 92expne0d 11267 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ( N  /  _e ) ^ N )  =/=  0 )
9472, 84, 89, 93mulne0d 9436 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) )  =/=  0 )
9567, 85, 94divcld 9552 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  CC )
9656, 64, 65, 95fvmptd 5622 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  e.  RR+ )  ->  ( A `  N
)  =  ( ( ! `  N )  /  ( ( sqr `  ( 2  x.  N
) )  x.  (
( N  /  _e ) ^ N ) ) ) )
9755, 96syl 15 . . . . . 6  |-  ( N  e.  NN  ->  ( A `  N )  =  ( ( ! `
 N )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
98 nfcv 2432 . . . . . . . . . 10  |-  F/_ k
( ( ! `  n )  /  (
( sqr `  (
2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) )
99 nfcv 2432 . . . . . . . . . 10  |-  F/_ n
( ( ! `  k )  /  (
( sqr `  (
2  x.  k ) )  x.  ( ( k  /  _e ) ^ k ) ) )
100 fveq2 5541 . . . . . . . . . . 11  |-  ( n  =  k  ->  ( ! `  n )  =  ( ! `  k ) )
101 oveq2 5882 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
102101fveq2d 5545 . . . . . . . . . . . 12  |-  ( n  =  k  ->  ( sqr `  ( 2  x.  n ) )  =  ( sqr `  (
2  x.  k ) ) )
103 oveq1 5881 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
n  /  _e )  =  ( k  /  _e ) )
104 id 19 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  n  =  k )
105103, 104oveq12d 5892 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( n  /  _e ) ^ n )  =  ( ( k  /  _e ) ^ k ) )
106102, 105oveq12d 5892 . . . . . . . . . . 11  |-  ( n  =  k  ->  (
( sqr `  (
2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) )  =  ( ( sqr `  ( 2  x.  k
) )  x.  (
( k  /  _e ) ^ k ) ) )
107100, 106oveq12d 5892 . . . . . . . . . 10  |-  ( n  =  k  ->  (
( ! `  n
)  /  ( ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^
n ) ) )  =  ( ( ! `
 k )  / 
( ( sqr `  (
2  x.  k ) )  x.  ( ( k  /  _e ) ^ k ) ) ) )
10898, 99, 107cbvmpt 4126 . . . . . . . . 9  |-  ( n  e.  NN  |->  ( ( ! `  n )  /  ( ( sqr `  ( 2  x.  n
) )  x.  (
( n  /  _e ) ^ n ) ) ) )  =  ( k  e.  NN  |->  ( ( ! `  k
)  /  ( ( sqr `  ( 2  x.  k ) )  x.  ( ( k  /  _e ) ^
k ) ) ) )
1091, 108eqtri 2316 . . . . . . . 8  |-  A  =  ( k  e.  NN  |->  ( ( ! `  k )  /  (
( sqr `  (
2  x.  k ) )  x.  ( ( k  /  _e ) ^ k ) ) ) )
110109a1i 10 . . . . . . 7  |-  ( N  e.  NN  ->  A  =  ( k  e.  NN  |->  ( ( ! `
 k )  / 
( ( sqr `  (
2  x.  k ) )  x.  ( ( k  /  _e ) ^ k ) ) ) ) )
11127fveq2d 5545 . . . . . . . 8  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( ! `  k )  =  ( ! `  ( N  +  1 ) ) )
11227oveq2d 5890 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( 2  x.  k )  =  ( 2  x.  ( N  +  1 ) ) )
113112fveq2d 5545 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( sqr `  (
2  x.  k ) )  =  ( sqr `  ( 2  x.  ( N  +  1 ) ) ) )
11427oveq1d 5889 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( k  /  _e )  =  (
( N  +  1 )  /  _e ) )
115114, 27oveq12d 5892 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( ( k  /  _e ) ^
k )  =  ( ( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )
116113, 115oveq12d 5892 . . . . . . . 8  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( ( sqr `  ( 2  x.  k
) )  x.  (
( k  /  _e ) ^ k ) )  =  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) )
117111, 116oveq12d 5892 . . . . . . 7  |-  ( ( N  e.  NN  /\  k  =  ( N  +  1 ) )  ->  ( ( ! `
 k )  / 
( ( sqr `  (
2  x.  k ) )  x.  ( ( k  /  _e ) ^ k ) ) )  =  ( ( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )
11830nnnn0d 10034 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  NN0 )
119 faccl 11314 . . . . . . . . 9  |-  ( ( N  +  1 )  e.  NN0  ->  ( ! `
 ( N  + 
1 ) )  e.  NN )
120 nnrp 10379 . . . . . . . . 9  |-  ( ( ! `  ( N  +  1 ) )  e.  NN  ->  ( ! `  ( N  +  1 ) )  e.  RR+ )
121118, 119, 1203syl 18 . . . . . . . 8  |-  ( N  e.  NN  ->  ( ! `  ( N  +  1 ) )  e.  RR+ )
122 nnre 9769 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  RR )
12339nn0ge0d 10037 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  0  <_  N )
124122, 123ge0p1rpd 10432 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  RR+ )
12544, 124rpmulcld 10422 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
2  x.  ( N  +  1 ) )  e.  RR+ )
126125rpsqrcld 11910 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  ( N  +  1 ) ) )  e.  RR+ )
127124, 49rpdivcld 10423 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  _e )  e.  RR+ )
12851peano2zd 10136 . . . . . . . . . 10  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  ZZ )
129127, 128rpexpcld 11284 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) )  e.  RR+ )
130126, 129rpmulcld 10422 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  e.  RR+ )
131121, 130rpdivcld 10423 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  e.  RR+ )
132110, 117, 30, 131fvmptd 5622 . . . . . 6  |-  ( N  e.  NN  ->  ( A `  ( N  +  1 ) )  =  ( ( ! `
 ( N  + 
1 ) )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )
13397, 132oveq12d 5892 . . . . 5  |-  ( N  e.  NN  ->  (
( A `  N
)  /  ( A `
 ( N  + 
1 ) ) )  =  ( ( ( ! `  N )  /  ( ( sqr `  ( 2  x.  N
) )  x.  (
( N  /  _e ) ^ N ) ) )  /  ( ( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )
134 facp1 11309 . . . . . . . . . 10  |-  ( N  e.  NN0  ->  ( ! `
 ( N  + 
1 ) )  =  ( ( ! `  N )  x.  ( N  +  1 ) ) )
13539, 134syl 15 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( ! `  ( N  +  1 ) )  =  ( ( ! `
 N )  x.  ( N  +  1 ) ) )
136135oveq1d 5889 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  =  ( ( ( ! `  N )  x.  ( N  + 
1 ) )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )
13730nncnd 9778 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  CC )
138130rpcnd 10408 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  e.  CC )
139130rpne0d 10411 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  =/=  0 )
14066, 137, 138, 139divassd 9587 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( ! `  N )  x.  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  =  ( ( ! `
 N )  x.  ( ( N  + 
1 )  /  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )
141136, 140eqtrd 2328 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  =  ( ( ! `
 N )  x.  ( ( N  + 
1 )  /  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )
142141oveq2d 5890 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  /  ( ( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =  ( ( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  /  ( ( ! `  N )  x.  ( ( N  +  1 )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) ) )
14353rpcnd 10408 . . . . . . 7  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) )  e.  CC )
144137, 138, 139divcld 9552 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  e.  CC )
14566, 144mulcld 8871 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ! `  N
)  x.  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  e.  CC )
14653rpne0d 10411 . . . . . . 7  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) )  =/=  0 )
14742rpne0d 10411 . . . . . . . 8  |-  ( N  e.  NN  ->  ( ! `  N )  =/=  0 )
14830nnne0d 9806 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( N  +  1 )  =/=  0 )
149137, 138, 148, 139divne0d 9568 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) )  =/=  0 )
15066, 144, 147, 149mulne0d 9436 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ! `  N
)  x.  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =/=  0
)
15166, 143, 145, 146, 150divdiv32d 9577 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  /  ( ( ! `  N )  x.  ( ( N  +  1 )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )  =  ( ( ( ! `
 N )  / 
( ( ! `  N )  x.  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) ) ) )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
15266, 66, 144, 147, 149divdiv1d 9583 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  ( ! `  N )
)  /  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =  ( ( ! `  N
)  /  ( ( ! `  N )  x.  ( ( N  +  1 )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) ) )
153152eqcomd 2301 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ! `  N
)  /  ( ( ! `  N )  x.  ( ( N  +  1 )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )  =  ( ( ( ! `
 N )  / 
( ! `  N
) )  /  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) ) ) )
154153oveq1d 5889 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  (
( ! `  N
)  x.  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( ! `  N )  /  ( ! `  N )
)  /  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
15566, 147dividd 9550 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ! `  N
)  /  ( ! `
 N ) )  =  1 )
156155oveq1d 5889 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  ( ! `  N )
)  /  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =  ( 1  /  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )
157156oveq1d 5889 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( ( ! `
 N )  / 
( ! `  N
) )  /  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) ) )  /  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( 1  /  ( ( N  +  1 )  / 
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
158137, 138, 148, 139recdivd 9569 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
1  /  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =  ( ( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) ) )
159158oveq1d 5889 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 1  /  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) ) )  /  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
160138, 137, 148divcld 9552 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  e.  CC )
16147rpcnd 10408 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  N ) )  e.  CC )
16252rpcnd 10408 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( N  /  _e ) ^ N )  e.  CC )
163161, 162, 146mulne0bad 9437 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  N ) )  =/=  0 )
164161, 162, 146mulne0bbd 9438 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( N  /  _e ) ^ N )  =/=  0 )
165160, 161, 162, 163, 164divdiv1d 9583 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) )  / 
( N  +  1 ) )  /  ( sqr `  ( 2  x.  N ) ) )  /  ( ( N  /  _e ) ^ N ) )  =  ( ( ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) )  / 
( N  +  1 ) )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) ) )
166165eqcomd 2301 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( sqr `  (
2  x.  N ) ) )  /  (
( N  /  _e ) ^ N ) ) )
167138, 137, 161, 148, 163divdiv32d 9577 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( sqr `  (
2  x.  N ) ) )  =  ( ( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( sqr `  (
2  x.  N ) ) )  /  ( N  +  1 ) ) )
168126rpcnd 10408 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  ( N  +  1 ) ) )  e.  CC )
169129rpcnd 10408 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) )  e.  CC )
170168, 169, 161, 163div23d 9589 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( sqr `  (
2  x.  N ) ) )  =  ( ( ( sqr `  (
2  x.  ( N  +  1 ) ) )  /  ( sqr `  ( 2  x.  N
) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  +  1 ) ) ) )
17144rpred 10406 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  2  e.  RR )
17244rpge0d 10410 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  0  <_  2 )
17330nnred 9777 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( N  +  1 )  e.  RR )
174118nn0ge0d 10037 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  0  <_  ( N  +  1 ) )
175171, 172, 173, 174sqrmuld 11923 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  ( N  +  1 ) ) )  =  ( ( sqr `  2
)  x.  ( sqr `  ( N  +  1 ) ) ) )
176171, 172, 122, 123sqrmuld 11923 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  ( sqr `  ( 2  x.  N ) )  =  ( ( sqr `  2
)  x.  ( sqr `  N ) ) )
177175, 176oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  /  ( sqr `  ( 2  x.  N
) ) )  =  ( ( ( sqr `  2 )  x.  ( sqr `  ( N  +  1 ) ) )  /  (
( sqr `  2
)  x.  ( sqr `  N ) ) ) )
17868a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  2  e.  CC )
179178sqrcld 11935 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  2 )  e.  CC )
180137sqrcld 11935 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  ( N  + 
1 ) )  e.  CC )
181 nncn 9770 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  e.  CC )
182181sqrcld 11935 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  N )  e.  CC )
18344rpsqrcld 11910 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( sqr `  2 )  e.  RR+ )
184 rpne0 10385 . . . . . . . . . . . . . . . . . 18  |-  ( ( sqr `  2 )  e.  RR+  ->  ( sqr `  2 )  =/=  0 )
185183, 184syl 15 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  2 )  =/=  0 )
18645rpsqrcld 11910 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( sqr `  N )  e.  RR+ )
187 rpne0 10385 . . . . . . . . . . . . . . . . . 18  |-  ( ( sqr `  N )  e.  RR+  ->  ( sqr `  N )  =/=  0
)
188186, 187syl 15 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  N )  =/=  0 )
189179, 179, 180, 182, 185, 188divmuldivd 9593 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( ( sqr `  2
)  /  ( sqr `  2 ) )  x.  ( ( sqr `  ( N  +  1 ) )  /  ( sqr `  N ) ) )  =  ( ( ( sqr `  2
)  x.  ( sqr `  ( N  +  1 ) ) )  / 
( ( sqr `  2
)  x.  ( sqr `  N ) ) ) )
190189eqcomd 2301 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  (
( ( sqr `  2
)  x.  ( sqr `  ( N  +  1 ) ) )  / 
( ( sqr `  2
)  x.  ( sqr `  N ) ) )  =  ( ( ( sqr `  2 )  /  ( sqr `  2
) )  x.  (
( sqr `  ( N  +  1 ) )  /  ( sqr `  N ) ) ) )
191179, 185dividd 9550 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( sqr `  2
)  /  ( sqr `  2 ) )  =  1 )
192173, 174, 45sqrdivd 11922 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( sqr `  ( ( N  +  1 )  /  N ) )  =  ( ( sqr `  ( N  +  1 ) )  /  ( sqr `  N ) ) )
193192eqcomd 2301 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( sqr `  ( N  +  1 ) )  /  ( sqr `  N ) )  =  ( sqr `  (
( N  +  1 )  /  N ) ) )
194191, 193oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  (
( ( sqr `  2
)  /  ( sqr `  2 ) )  x.  ( ( sqr `  ( N  +  1 ) )  /  ( sqr `  N ) ) )  =  ( 1  x.  ( sqr `  (
( N  +  1 )  /  N ) ) ) )
195177, 190, 1943eqtrd 2332 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( sqr `  (
2  x.  ( N  +  1 ) ) )  /  ( sqr `  ( 2  x.  N
) ) )  =  ( 1  x.  ( sqr `  ( ( N  +  1 )  /  N ) ) ) )
196195oveq1d 5889 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  /  ( sqr `  ( 2  x.  N
) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  +  1 ) ) )  =  ( ( 1  x.  ( sqr `  ( ( N  + 
1 )  /  N
) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  +  1 ) ) ) )
197 nnne0 9794 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  N  =/=  0 )
198137, 181, 197divcld 9552 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  N )  e.  CC )
199198sqrcld 11935 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  ( sqr `  ( ( N  +  1 )  /  N ) )  e.  CC )
200199mulid2d 8869 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
1  x.  ( sqr `  ( ( N  + 
1 )  /  N
) ) )  =  ( sqr `  (
( N  +  1 )  /  N ) ) )
201200oveq1d 5889 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( 1  x.  ( sqr `  ( ( N  +  1 )  /  N ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) )
202170, 196, 2013eqtrd 2332 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( sqr `  (
2  x.  ( N  +  1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( sqr `  (
2  x.  N ) ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) ) )
203202oveq1d 5889 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( sqr `  (
2  x.  N ) ) )  /  ( N  +  1 ) )  =  ( ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) ) )
204167, 203eqtrd 2328 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( sqr `  (
2  x.  N ) ) )  =  ( ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) ) )
205204oveq1d 5889 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) )  / 
( N  +  1 ) )  /  ( sqr `  ( 2  x.  N ) ) )  /  ( ( N  /  _e ) ^ N ) )  =  ( ( ( ( sqr `  ( ( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) )  / 
( N  +  1 ) )  /  (
( N  /  _e ) ^ N ) ) )
206166, 205eqtrd 2328 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( N  /  _e ) ^ N ) ) )
207199, 169mulcld 8871 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  e.  CC )
208207, 137, 162, 148, 164divdiv32d 9577 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( N  /  _e ) ^ N ) )  =  ( ( ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( ( N  /  _e ) ^ N ) )  / 
( N  +  1 ) ) )
209199, 169, 162, 164divassd 9587 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( ( N  /  _e ) ^ N ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) )  / 
( ( N  /  _e ) ^ N ) ) ) )
21049rpcnd 10408 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  _e  e.  CC )
21149rpne0d 10411 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  _e  =/=  0 )
212137, 210, 211, 118expdivd 11275 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) )  =  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  (
_e ^ ( N  +  1 ) ) ) )
213181, 210, 211, 39expdivd 11275 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( N  /  _e ) ^ N )  =  ( ( N ^ N )  /  (
_e ^ N ) ) )
214212, 213oveq12d 5892 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 )  /  _e ) ^ ( N  +  1 ) )  /  ( ( N  /  _e ) ^ N ) )  =  ( ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( _e ^ ( N  +  1 ) ) )  /  (
( N ^ N
)  /  ( _e
^ N ) ) ) )
215214oveq2d 5890 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) )  / 
( ( N  /  _e ) ^ N ) ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( _e
^ ( N  + 
1 ) ) )  /  ( ( N ^ N )  / 
( _e ^ N
) ) ) ) )
216137, 118expcld 11261 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( N  +  1 ) ^ ( N  +  1 ) )  e.  CC )
217210, 118expcld 11261 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
_e ^ ( N  +  1 ) )  e.  CC )
218181, 39expcld 11261 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  ( N ^ N )  e.  CC )
219210, 39expcld 11261 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
_e ^ N )  e.  CC )
220210, 211, 128expne0d 11267 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
_e ^ ( N  +  1 ) )  =/=  0 )
221210, 211, 51expne0d 11267 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
_e ^ N )  =/=  0 )
222181, 197, 51expne0d 11267 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  ( N ^ N )  =/=  0 )
223216, 217, 218, 219, 220, 221, 222divdivdivd 9599 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  (
_e ^ ( N  +  1 ) ) )  /  ( ( N ^ N )  /  ( _e ^ N ) ) )  =  ( ( ( ( N  +  1 ) ^ ( N  +  1 ) )  x.  ( _e ^ N ) )  / 
( ( _e ^
( N  +  1 ) )  x.  ( N ^ N ) ) ) )
224216, 219mulcomd 8872 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( N  + 
1 ) ^ ( N  +  1 ) )  x.  ( _e
^ N ) )  =  ( ( _e
^ N )  x.  ( ( N  + 
1 ) ^ ( N  +  1 ) ) ) )
225224oveq1d 5889 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  x.  (
_e ^ N ) )  /  ( ( _e ^ ( N  +  1 ) )  x.  ( N ^ N ) ) )  =  ( ( ( _e ^ N )  x.  ( ( N  +  1 ) ^
( N  +  1 ) ) )  / 
( ( _e ^
( N  +  1 ) )  x.  ( N ^ N ) ) ) )
226219, 217, 216, 218, 220, 222divmuldivd 9593 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  /  (
_e ^ ( N  +  1 ) ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  =  ( ( ( _e ^ N )  x.  ( ( N  +  1 ) ^
( N  +  1 ) ) )  / 
( ( _e ^
( N  +  1 ) )  x.  ( N ^ N ) ) ) )
227226eqcomd 2301 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  x.  (
( N  +  1 ) ^ ( N  +  1 ) ) )  /  ( ( _e ^ ( N  +  1 ) )  x.  ( N ^ N ) ) )  =  ( ( ( _e ^ N )  /  ( _e ^
( N  +  1 ) ) )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) ) )
228210, 39expp1d 11262 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  (
_e ^ ( N  +  1 ) )  =  ( ( _e
^ N )  x.  _e ) )
229228oveq2d 5890 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( _e ^ N
)  /  ( _e
^ ( N  + 
1 ) ) )  =  ( ( _e
^ N )  / 
( ( _e ^ N )  x.  _e ) ) )
230219, 219, 210, 221, 211divdiv1d 9583 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  /  (
_e ^ N ) )  /  _e )  =  ( ( _e
^ N )  / 
( ( _e ^ N )  x.  _e ) ) )
231230eqcomd 2301 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( _e ^ N
)  /  ( ( _e ^ N )  x.  _e ) )  =  ( ( ( _e ^ N )  /  ( _e ^ N ) )  /  _e ) )
232219, 221dividd 9550 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  (
( _e ^ N
)  /  ( _e
^ N ) )  =  1 )
233232oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  /  (
_e ^ N ) )  /  _e )  =  ( 1  /  _e ) )
234229, 231, 2333eqtrd 2332 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  (
( _e ^ N
)  /  ( _e
^ ( N  + 
1 ) ) )  =  ( 1  /  _e ) )
235234oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  /  (
_e ^ ( N  +  1 ) ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  =  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) ) )
236227, 235eqtrd 2328 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( _e ^ N )  x.  (
( N  +  1 ) ^ ( N  +  1 ) ) )  /  ( ( _e ^ ( N  +  1 ) )  x.  ( N ^ N ) ) )  =  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) ) )
237223, 225, 2363eqtrd 2332 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  (
_e ^ ( N  +  1 ) ) )  /  ( ( N ^ N )  /  ( _e ^ N ) ) )  =  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) ) )
238237oveq2d 5890 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( _e
^ ( N  + 
1 ) ) )  /  ( ( N ^ N )  / 
( _e ^ N
) ) ) )  =  ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( 1  /  _e )  x.  ( (
( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) ) ) )
239209, 215, 2383eqtrd 2332 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( ( N  /  _e ) ^ N ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) ) ) )
240239oveq1d 5889 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( ( N  /  _e ) ^ N ) )  / 
( N  +  1 ) )  =  ( ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) ) )  /  ( N  + 
1 ) ) )
241210, 211reccld 9545 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
1  /  _e )  e.  CC )
242216, 218, 222divcld 9552 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  e.  CC )
243241, 242mulcld 8871 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( 1  /  _e )  x.  ( (
( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  e.  CC )
244199, 243, 137, 148div23d 9589 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) ) )  /  ( N  + 
1 ) )  =  ( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) ) ) )
245 ax-1cn 8811 . . . . . . . . . . . . . 14  |-  1  e.  CC
246245a1i 10 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  1  e.  CC )
247246, 210, 242, 211div32d 9575 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( 1  /  _e )  x.  ( (
( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  =  ( 1  x.  ( ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) )  /  _e ) ) )
248242, 210, 211divcld 9552 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) )  /  _e )  e.  CC )
249248mulid2d 8869 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
1  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) )  =  ( ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) )
250247, 249eqtrd 2328 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( 1  /  _e )  x.  ( (
( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  =  ( ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) )
251250oveq2d 5890 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) ) )  =  ( ( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) ) )
252199, 137, 148divcld 9552 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  e.  CC )
253252, 242, 210, 211divassd 9587 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  /  _e )  =  ( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) ) )
254253eqcomd 2301 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  _e ) )  =  ( ( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  /  _e ) )
255244, 251, 2543eqtrd 2332 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( 1  /  _e )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) ) )  /  ( N  + 
1 ) )  =  ( ( ( ( sqr `  ( ( N  +  1 )  /  N ) )  /  ( N  + 
1 ) )  x.  ( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) ) )  /  _e ) )
256208, 240, 2553eqtrd 2332 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) )  /  ( N  + 
1 ) )  / 
( ( N  /  _e ) ^ N ) )  =  ( ( ( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) )  /  _e ) )
257159, 206, 2563eqtrd 2332 . . . . . . 7  |-  ( N  e.  NN  ->  (
( 1  /  (
( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  + 
1 ) ) )  x.  ( ( ( N  +  1 )  /  _e ) ^
( N  +  1 ) ) ) ) )  /  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) )  /  _e ) )
258154, 157, 2573eqtrd 2332 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  (
( ! `  N
)  x.  ( ( N  +  1 )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) ) )  / 
( ( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  =  ( ( ( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) )  /  _e ) )
259142, 151, 2583eqtrd 2332 . . . . 5  |-  ( N  e.  NN  ->  (
( ( ! `  N )  /  (
( sqr `  (
2  x.  N ) )  x.  ( ( N  /  _e ) ^ N ) ) )  /  ( ( ! `  ( N  +  1 ) )  /  ( ( sqr `  ( 2  x.  ( N  +  1 ) ) )  x.  (
( ( N  + 
1 )  /  _e ) ^ ( N  + 
1 ) ) ) ) )  =  ( ( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  /  _e ) )
260199, 137, 242, 148div32d 9575 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  ( N  + 
1 ) ) ) )
261216, 218, 137, 222, 148divdiv32d 9577 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) )  /  ( N  + 
1 ) )  =  ( ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N  +  1 ) )  /  ( N ^ N ) ) )
262137, 39expp1d 11262 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( N  +  1 ) ^ ( N  +  1 ) )  =  ( ( ( N  +  1 ) ^ N )  x.  ( N  +  1 ) ) )
263262oveq1d 5889 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N  +  1 ) )  =  ( ( ( ( N  +  1 ) ^ N )  x.  ( N  + 
1 ) )  / 
( N  +  1 ) ) )
264137, 39expcld 11261 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( N  +  1 ) ^ N )  e.  CC )
265264, 137, 148divcan4d 9558 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^ N )  x.  ( N  +  1 ) )  /  ( N  +  1 ) )  =  ( ( N  +  1 ) ^ N ) )
266263, 265eqtrd 2328 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N  +  1 ) )  =  ( ( N  +  1 ) ^ N ) )
267266oveq1d 5889 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N  +  1 ) )  /  ( N ^ N ) )  =  ( ( ( N  +  1 ) ^ N )  / 
( N ^ N
) ) )
268137, 181, 197, 39expdivd 11275 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  N
) ^ N )  =  ( ( ( N  +  1 ) ^ N )  / 
( N ^ N
) ) )
269268eqcomd 2301 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( ( N  + 
1 ) ^ N
)  /  ( N ^ N ) )  =  ( ( ( N  +  1 )  /  N ) ^ N ) )
270261, 267, 2693eqtrd 2332 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( ( N  +  1 ) ^
( N  +  1 ) )  /  ( N ^ N ) )  /  ( N  + 
1 ) )  =  ( ( ( N  +  1 )  /  N ) ^ N
) )
271270oveq2d 5890 . . . . . . 7  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( ( N  + 
1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) )  /  ( N  + 
1 ) ) )  =  ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  N
) ^ N ) ) )
272260, 271eqtrd 2328 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( sqr `  (
( N  +  1 )  /  N ) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  + 
1 ) )  / 
( N ^ N
) ) )  =  ( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) ) )
273272oveq1d 5889 . . . . 5  |-  ( N  e.  NN  ->  (
( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  /  ( N  +  1 ) )  x.  ( ( ( N  +  1 ) ^ ( N  +  1 ) )  /  ( N ^ N ) ) )  /  _e )  =  ( ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  N
) ^ N ) )  /  _e ) )
274133, 259, 2733eqtrd 2332 . . . 4  |-  ( N  e.  NN  ->  (
( A `  N
)  /  ( A `
 ( N  + 
1 ) ) )  =  ( ( ( sqr `  ( ( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  /  _e ) )
275274fveq2d 5545 . . 3  |-  ( N  e.  NN  ->  ( log `  ( ( A `
 N )  / 
( A `  ( N  +  1 ) ) ) )  =  ( log `  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  /  _e ) ) )
27635, 37, 2753eqtrd 2332 . 2  |-  ( N  e.  NN  ->  (
( B `  N
)  -  ( B `
 ( N  + 
1 ) ) )  =  ( log `  (
( ( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  /  _e ) ) )
277124, 45rpdivcld 10423 . . . . . 6  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  N )  e.  RR+ )
278277rpsqrcld 11910 . . . . 5  |-  ( N  e.  NN  ->  ( sqr `  ( ( N  +  1 )  /  N ) )  e.  RR+ )
279277, 51rpexpcld 11284 . . . . 5  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  N
) ^ N )  e.  RR+ )
280278, 279rpmulcld 10422 . . . 4  |-  ( N  e.  NN  ->  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  e.  RR+ )
281280, 49relogdivd 19993 . . 3  |-  ( N  e.  NN  ->  ( log `  ( ( ( sqr `  ( ( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  /  _e ) )  =  ( ( log `  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) ) )  -  ( log `  _e ) ) )
282278, 279relogmuld 19992 . . . . . 6  |-  ( N  e.  NN  ->  ( log `  ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  N
) ^ N ) ) )  =  ( ( log `  ( sqr `  ( ( N  +  1 )  /  N ) ) )  +  ( log `  (
( ( N  + 
1 )  /  N
) ^ N ) ) ) )
283 logsqr 20067 . . . . . . . 8  |-  ( ( ( N  +  1 )  /  N )  e.  RR+  ->  ( log `  ( sqr `  (
( N  +  1 )  /  N ) ) )  =  ( ( log `  (
( N  +  1 )  /  N ) )  /  2 ) )
284277, 283syl 15 . . . . . . 7  |-  ( N  e.  NN  ->  ( log `  ( sqr `  (
( N  +  1 )  /  N ) ) )  =  ( ( log `  (
( N  +  1 )  /  N ) )  /  2 ) )
285277, 51jca 518 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( N  + 
1 )  /  N
)  e.  RR+  /\  N  e.  ZZ ) )
286 relogexp 19965 . . . . . . . 8  |-  ( ( ( ( N  + 
1 )  /  N
)  e.  RR+  /\  N  e.  ZZ )  ->  ( log `  ( ( ( N  +  1 )  /  N ) ^ N ) )  =  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )
287285, 286syl 15 . . . . . . 7  |-  ( N  e.  NN  ->  ( log `  ( ( ( N  +  1 )  /  N ) ^ N ) )  =  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )
288284, 287oveq12d 5892 . . . . . 6  |-  ( N  e.  NN  ->  (
( log `  ( sqr `  ( ( N  +  1 )  /  N ) ) )  +  ( log `  (
( ( N  + 
1 )  /  N
) ^ N ) ) )  =  ( ( ( log `  (
( N  +  1 )  /  N ) )  /  2 )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) ) )
289282, 288eqtrd 2328 . . . . 5  |-  ( N  e.  NN  ->  ( log `  ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  N
) ^ N ) ) )  =  ( ( ( log `  (
( N  +  1 )  /  N ) )  /  2 )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) ) )
290137, 181, 148, 197divne0d 9568 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( N  +  1 )  /  N )  =/=  0 )
291198, 290logcld 19944 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( log `  ( ( N  +  1 )  /  N ) )  e.  CC )
292246halfcld 9972 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
1  /  2 )  e.  CC )
29344rpne0d 10411 . . . . . . . . 9  |-  ( N  e.  NN  ->  2  =/=  0 )
294178, 293recne0d 9546 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
1  /  2 )  =/=  0 )
295291, 178, 292, 293, 294divcan5d 9578 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  /  ( ( 1  /  2 )  x.  2 ) )  =  ( ( log `  (
( N  +  1 )  /  N ) )  /  2 ) )
296295eqcomd 2301 . . . . . . 7  |-  ( N  e.  NN  ->  (
( log `  (
( N  +  1 )  /  N ) )  /  2 )  =  ( ( ( 1  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  /  (
( 1  /  2
)  x.  2 ) ) )
297178, 293recid2d 9548 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 1  /  2
)  x.  2 )  =  1 )
298297oveq2d 5890 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  /  ( ( 1  /  2 )  x.  2 ) )  =  ( ( ( 1  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  /  1
) )
299292, 291mulcld 8871 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 1  /  2
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) )  e.  CC )
300299div1d 9544 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  /  1 )  =  ( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )
301296, 298, 3003eqtrd 2332 . . . . . 6  |-  ( N  e.  NN  ->  (
( log `  (
( N  +  1 )  /  N ) )  /  2 )  =  ( ( 1  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) ) )
302301oveq1d 5889 . . . . 5  |-  ( N  e.  NN  ->  (
( ( log `  (
( N  +  1 )  /  N ) )  /  2 )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )  =  ( ( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) ) )
303292, 181, 291adddird 8876 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  +  N
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) )  =  ( ( ( 1  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  +  ( N  x.  ( log `  ( ( N  + 
1 )  /  N
) ) ) ) )
304303eqcomd 2301 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )  =  ( ( ( 1  / 
2 )  +  N
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) ) )
305181, 178, 293divcan4d 9558 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( N  x.  2 )  /  2 )  =  N )
306305eqcomd 2301 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  =  ( ( N  x.  2 )  / 
2 ) )
307181, 178mulcomd 8872 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( N  x.  2 )  =  ( 2  x.  N ) )
308307oveq1d 5889 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( N  x.  2 )  /  2 )  =  ( ( 2  x.  N )  / 
2 ) )
309306, 308eqtrd 2328 . . . . . . . . 9  |-  ( N  e.  NN  ->  N  =  ( ( 2  x.  N )  / 
2 ) )
310309oveq2d 5890 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 1  /  2
)  +  N )  =  ( ( 1  /  2 )  +  ( ( 2  x.  N )  /  2
) ) )
311178, 181mulcld 8871 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
2  x.  N )  e.  CC )
312246, 311, 178, 293divdird 9590 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( 1  +  ( 2  x.  N ) )  /  2 )  =  ( ( 1  /  2 )  +  ( ( 2  x.  N )  /  2
) ) )
313312eqcomd 2301 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 1  /  2
)  +  ( ( 2  x.  N )  /  2 ) )  =  ( ( 1  +  ( 2  x.  N ) )  / 
2 ) )
314310, 313eqtrd 2328 . . . . . . 7  |-  ( N  e.  NN  ->  (
( 1  /  2
)  +  N )  =  ( ( 1  +  ( 2  x.  N ) )  / 
2 ) )
315314oveq1d 5889 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  +  N
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) )  =  ( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )
316304, 315eqtrd 2328 . . . . 5  |-  ( N  e.  NN  ->  (
( ( 1  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  +  ( N  x.  ( log `  ( ( N  +  1 )  /  N ) ) ) )  =  ( ( ( 1  +  ( 2  x.  N
) )  /  2
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) ) )
317289, 302, 3163eqtrd 2332 . . . 4  |-  ( N  e.  NN  ->  ( log `  ( ( sqr `  ( ( N  + 
1 )  /  N
) )  x.  (
( ( N  + 
1 )  /  N
) ^ N ) ) )  =  ( ( ( 1  +  ( 2  x.  N
) )  /  2
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) ) )
318 loge 19956 . . . . 5  |-  ( log `  _e )  =  1
319318a1i 10 . . . 4  |-  ( N  e.  NN  ->  ( log `  _e )  =  1 )
320317, 319oveq12d 5892 . . 3  |-  ( N  e.  NN  ->  (
( log `  (
( sqr `  (
( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) ) )  -  ( log `  _e ) )  =  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 ) )
321281, 320eqtrd 2328 . 2  |-  ( N  e.  NN  ->  ( log `  ( ( ( sqr `  ( ( N  +  1 )  /  N ) )  x.  ( ( ( N  +  1 )  /  N ) ^ N ) )  /  _e ) )  =  ( ( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 ) )
322246, 311addcld 8870 . . . . . . . 8  |-  ( N  e.  NN  ->  (
1  +  ( 2  x.  N ) )  e.  CC )
323322halfcld 9972 . . . . . . 7  |-  ( N  e.  NN  ->  (
( 1  +  ( 2  x.  N ) )  /  2 )  e.  CC )
324323, 291mulcld 8871 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( 1  +  ( 2  x.  N
) )  /  2
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) )  e.  CC )
325324, 246subcld 9173 . . . . 5  |-  ( N  e.  NN  ->  (
( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )
32638, 325jca 518 . . . 4  |-  ( N  e.  NN  ->  ( N  e.  NN  /\  (
( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 )  e.  CC ) )
327 stirlinglem4.3 . . . . . 6  |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  ( 2  x.  n ) )  /  2 )  x.  ( log `  (
( n  +  1 )  /  n ) ) )  -  1 ) )
328327a1i 10 . . . . 5  |-  ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  ->  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  ( 2  x.  n ) )  / 
2 )  x.  ( log `  ( ( n  +  1 )  /  n ) ) )  -  1 ) ) )
329 simpr 447 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  n  =  N )
330329oveq2d 5890 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( 2  x.  n )  =  ( 2  x.  N
) )
331330oveq2d 5890 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( 1  +  ( 2  x.  n ) )  =  ( 1  +  ( 2  x.  N ) ) )
332331oveq1d 5889 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( (
1  +  ( 2  x.  n ) )  /  2 )  =  ( ( 1  +  ( 2  x.  N
) )  /  2
) )
333329oveq1d 5889 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( n  +  1 )  =  ( N  +  1 ) )
334333, 329oveq12d 5892 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( (
n  +  1 )  /  n )  =  ( ( N  + 
1 )  /  N
) )
335334fveq2d 5545 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( log `  ( ( n  + 
1 )  /  n
) )  =  ( log `  ( ( N  +  1 )  /  N ) ) )
336332, 335oveq12d 5892 . . . . . 6  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( (
( 1  +  ( 2  x.  n ) )  /  2 )  x.  ( log `  (
( n  +  1 )  /  n ) ) )  =  ( ( ( 1  +  ( 2  x.  N
) )  /  2
)  x.  ( log `  ( ( N  + 
1 )  /  N
) ) ) )
337336oveq1d 5889 . . . . 5  |-  ( ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  /\  n  =  N )  ->  ( (
( ( 1  +  ( 2  x.  n
) )  /  2
)  x.  ( log `  ( ( n  + 
1 )  /  n
) ) )  - 
1 )  =  ( ( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 ) )
338 simpl 443 . . . . 5  |-  ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  ->  N  e.  NN )
339338, 325syl 15 . . . . 5  |-  ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  ->  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )
340328, 337, 338, 339fvmptd 5622 . . . 4  |-  ( ( N  e.  NN  /\  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 )  e.  CC )  ->  ( J `  N )  =  ( ( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 ) )
341326, 340syl 15 . . 3  |-  ( N  e.  NN  ->  ( J `  N )  =  ( ( ( ( 1  +  ( 2  x.  N ) )  /  2 )  x.  ( log `  (
( N  +  1 )  /  N ) ) )  -  1 ) )
342341eqcomd 2301 . 2  |-  ( N  e.  NN  ->  (
( ( ( 1  +  ( 2  x.  N ) )  / 
2 )  x.  ( log `  ( ( N  +  1 )  /  N ) ) )  -  1 )  =  ( J `  N
) )
343276, 321, 3423eqtrd 2332 1  |-  ( N  e.  NN  ->  (
( B `  N
)  -  ( B `
 ( N  + 
1 ) ) )  =  ( J `  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   class class class wbr 4039    e. cmpt 4093   ` cfv 5271  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    < clt 8883    - cmin 9053    / cdiv 9439   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   RR+crp 10370   ^cexp 11120   !cfa 11304   sqrcsqr 11734   _eceu 12360   logclog 19928
This theorem is referenced by:  stirlinglem9  27934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14