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

Theorem leibpi 20743
Description: The Leibniz formula for  pi. This proof depends on three main facts: (1) the series  F is convergent, because it is an alternating series (iseralt 12441). (2) Using leibpilem2 20742 to rewrite the series as a power series, it is the  x  =  1 special case of the Taylor series for arctan (atantayl2 20739). (3) Although we cannot directly plug  x  =  1 into atantayl2 20739, Abel's theorem (abelth2 20319) says that the limit along any sequence converging to  1, such as 
1  -  1  /  n, of the power series converges to the power series extended to  1, and then since arctan is continuous at  1 (atancn 20737) we get the desired result. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
leibpi.1  |-  F  =  ( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) )
Assertion
Ref Expression
leibpi  |-  seq  0
(  +  ,  F
)  ~~>  ( pi  / 
4 )

Proof of Theorem leibpi
Dummy variables  j 
k  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 10484 . . . . 5  |-  NN0  =  ( ZZ>= `  0 )
2 0z 10257 . . . . . 6  |-  0  e.  ZZ
32a1i 11 . . . . 5  |-  (  T. 
->  0  e.  ZZ )
4 eqidd 2413 . . . . 5  |-  ( (  T.  /\  j  e. 
NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  =  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j ) )
5 0cn 9048 . . . . . . . . . 10  |-  0  e.  CC
65a1i 11 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  ( k  =  0  \/  2  ||  k
) )  ->  0  e.  CC )
7 ioran 477 . . . . . . . . . 10  |-  ( -.  ( k  =  0  \/  2  ||  k
)  <->  ( -.  k  =  0  /\  -.  2  ||  k ) )
8 1re 9054 . . . . . . . . . . . . . 14  |-  1  e.  RR
98renegcli 9326 . . . . . . . . . . . . 13  |-  -u 1  e.  RR
10 leibpilem1 20741 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( k  e.  NN  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )
)
1110simprd 450 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( k  - 
1 )  /  2
)  e.  NN0 )
12 reexpcl 11361 . . . . . . . . . . . . 13  |-  ( (
-u 1  e.  RR  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  e.  RR )
139, 11, 12sylancr 645 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( -u 1 ^ (
( k  -  1 )  /  2 ) )  e.  RR )
1410simpld 446 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
k  e.  NN )
1513, 14nndivred 10012 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  RR )
1615recnd 9078 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  CC )
177, 16sylan2b 462 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  -.  ( k  =  0  \/  2  ||  k
) )  ->  (
( -u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  CC )
186, 17ifclda 3734 . . . . . . . 8  |-  ( k  e.  NN0  ->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e.  CC )
1918adantl 453 . . . . . . 7  |-  ( (  T.  /\  k  e. 
NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  e.  CC )
20 eqid 2412 . . . . . . 7  |-  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) )  =  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) )
2119, 20fmptd 5860 . . . . . 6  |-  (  T. 
->  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) : NN0 --> CC )
2221ffvelrnda 5837 . . . . 5  |-  ( (  T.  /\  j  e. 
NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  e.  CC )
23 2nn0 10202 . . . . . . . . . . . . . 14  |-  2  e.  NN0
2423a1i 11 . . . . . . . . . . . . 13  |-  (  T. 
->  2  e.  NN0 )
25 nn0mulcl 10220 . . . . . . . . . . . . 13  |-  ( ( 2  e.  NN0  /\  n  e.  NN0 )  -> 
( 2  x.  n
)  e.  NN0 )
2624, 25sylan 458 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
2  x.  n )  e.  NN0 )
27 nn0p1nn 10223 . . . . . . . . . . . 12  |-  ( ( 2  x.  n )  e.  NN0  ->  ( ( 2  x.  n )  +  1 )  e.  NN )
2826, 27syl 16 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
2928nnrecred 10009 . . . . . . . . . 10  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  e.  RR )
30 eqid 2412 . . . . . . . . . 10  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) )
3129, 30fmptd 5860 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) : NN0 --> RR )
32 nn0mulcl 10220 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  k  e.  NN0 )  -> 
( 2  x.  k
)  e.  NN0 )
3324, 32sylan 458 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  NN0 )
3433nn0red 10239 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  RR )
35 peano2nn0 10224 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
3635adantl 453 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  NN0 )
37 nn0mulcl 10220 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  ( k  +  1 )  e.  NN0 )  ->  ( 2  x.  (
k  +  1 ) )  e.  NN0 )
3823, 36, 37sylancr 645 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  NN0 )
3938nn0red 10239 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  RR )
408a1i 11 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  1  e.  RR )
41 nn0re 10194 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  k  e.  RR )
4241adantl 453 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  e.  RR )
4342lep1d 9906 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  <_  ( k  +  1 ) )
44 peano2re 9203 . . . . . . . . . . . . . . 15  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
4542, 44syl 16 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  RR )
46 2re 10033 . . . . . . . . . . . . . . 15  |-  2  e.  RR
4746a1i 11 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  2  e.  RR )
48 2pos 10046 . . . . . . . . . . . . . . 15  |-  0  <  2
4948a1i 11 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  2 )
50 lemul2 9827 . . . . . . . . . . . . . 14  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( k  <_  ( k  +  1 )  <->  ( 2  x.  k )  <_  (
2  x.  ( k  +  1 ) ) ) )
5142, 45, 47, 49, 50syl112anc 1188 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  <_  ( k  +  1 )  <->  ( 2  x.  k )  <_ 
( 2  x.  (
k  +  1 ) ) ) )
5243, 51mpbid 202 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  <_  ( 2  x.  ( k  +  1 ) ) )
5334, 39, 40, 52leadd1dd 9604 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  <_  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
54 nn0p1nn 10223 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
5533, 54syl 16 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
5655nnred 9979 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
5755nngt0d 10007 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
58 nn0p1nn 10223 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  ( k  +  1 ) )  e.  NN0  ->  ( ( 2  x.  ( k  +  1 ) )  +  1 )  e.  NN )
5938, 58syl 16 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  NN )
6059nnred 9979 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  RR )
6159nngt0d 10007 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
62 lerec 9856 . . . . . . . . . . . 12  |-  ( ( ( ( ( 2  x.  k )  +  1 )  e.  RR  /\  0  <  ( ( 2  x.  k )  +  1 ) )  /\  ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  e.  RR  /\  0  < 
( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )  -> 
( ( ( 2  x.  k )  +  1 )  <_  (
( 2  x.  (
k  +  1 ) )  +  1 )  <-> 
( 1  /  (
( 2  x.  (
k  +  1 ) )  +  1 ) )  <_  ( 1  /  ( ( 2  x.  k )  +  1 ) ) ) )
6356, 57, 60, 61, 62syl22anc 1185 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( ( 2  x.  k )  +  1 )  <_  ( (
2  x.  ( k  +  1 ) )  +  1 )  <->  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  <_ 
( 1  /  (
( 2  x.  k
)  +  1 ) ) ) )
6453, 63mpbid 202 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  <_  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
65 oveq2 6056 . . . . . . . . . . . . . 14  |-  ( n  =  ( k  +  1 )  ->  (
2  x.  n )  =  ( 2  x.  ( k  +  1 ) ) )
6665oveq1d 6063 . . . . . . . . . . . . 13  |-  ( n  =  ( k  +  1 )  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
6766oveq2d 6064 . . . . . . . . . . . 12  |-  ( n  =  ( k  +  1 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
68 ovex 6073 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  e. 
_V
6967, 30, 68fvmpt 5773 . . . . . . . . . . 11  |-  ( ( k  +  1 )  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 ( k  +  1 ) )  =  ( 1  /  (
( 2  x.  (
k  +  1 ) )  +  1 ) ) )
7036, 69syl 16 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  (
k  +  1 ) )  =  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
71 oveq2 6056 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
7271oveq1d 6063 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  k )  +  1 ) )
7372oveq2d 6064 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
74 ovex 6073 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  k )  +  1 ) )  e. 
_V
7573, 30, 74fvmpt 5773 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k )  =  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
7675adantl 453 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
7764, 70, 763brtr4d 4210 . . . . . . . . 9  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  (
k  +  1 ) )  <_  ( (
n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k ) )
78 nnuz 10485 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
79 1z 10275 . . . . . . . . . . 11  |-  1  e.  ZZ
8079a1i 11 . . . . . . . . . 10  |-  (  T. 
->  1  e.  ZZ )
81 ax-1cn 9012 . . . . . . . . . . 11  |-  1  e.  CC
82 divcnv 12596 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  (
n  e.  NN  |->  ( 1  /  n ) )  ~~>  0 )
8381, 82mp1i 12 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  /  n
) )  ~~>  0 )
84 nn0ex 10191 . . . . . . . . . . . 12  |-  NN0  e.  _V
8584mptex 5933 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  e.  _V
8685a1i 11 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  e.  _V )
87 oveq2 6056 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
1  /  n )  =  ( 1  / 
k ) )
88 eqid 2412 . . . . . . . . . . . . 13  |-  ( n  e.  NN  |->  ( 1  /  n ) )  =  ( n  e.  NN  |->  ( 1  /  n ) )
89 ovex 6073 . . . . . . . . . . . . 13  |-  ( 1  /  k )  e. 
_V
9087, 88, 89fvmpt 5773 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
9190adantl 453 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
92 nnrecre 10000 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
9392adantl 453 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  k )  e.  RR )
9491, 93eqeltrd 2486 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  RR )
95 nnnn0 10192 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  NN0 )
9695adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  NN0 )
9796, 75syl 16 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
9895, 55sylan2 461 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
9998nnrecred 10009 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR )
10097, 99eqeltrd 2486 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  e.  RR )
101 nnre 9971 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  k  e.  RR )
102101adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  RR )
10323, 96, 32sylancr 645 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  NN0 )
104103nn0red 10239 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  RR )
105 peano2re 9203 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  RR  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
106104, 105syl 16 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
107 nn0addge1 10230 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  RR  /\  k  e.  NN0 )  -> 
k  <_  ( k  +  k ) )
108102, 96, 107syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( k  +  k ) )
109102recnd 9078 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  CC )
1101092timesd 10174 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  =  ( k  +  k ) )
111108, 110breqtrrd 4206 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( 2  x.  k
) )
112104lep1d 9906 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  <_  ( ( 2  x.  k )  +  1 ) )
113102, 104, 106, 111, 112letrd 9191 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( ( 2  x.  k )  +  1 ) )
114 nngt0 9993 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  0  <  k )
115114adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  k )
11698nnred 9979 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
11798nngt0d 10007 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
118 lerec 9856 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  RR  /\  0  <  k )  /\  ( ( ( 2  x.  k )  +  1 )  e.  RR  /\  0  < 
( ( 2  x.  k )  +  1 ) ) )  -> 
( k  <_  (
( 2  x.  k
)  +  1 )  <-> 
( 1  /  (
( 2  x.  k
)  +  1 ) )  <_  ( 1  /  k ) ) )
119102, 115, 116, 117, 118syl22anc 1185 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
k  <_  ( (
2  x.  k )  +  1 )  <->  ( 1  /  ( ( 2  x.  k )  +  1 ) )  <_ 
( 1  /  k
) ) )
120113, 119mpbid 202 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  <_  ( 1  / 
k ) )
121120, 97, 913brtr4d 4210 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  <_  ( (
n  e.  NN  |->  ( 1  /  n ) ) `  k ) )
12298nnrpd 10611 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR+ )
123122rpreccld 10622 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR+ )
124123rpge0d 10616 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
125124, 97breqtrrd 4206 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) ) `  k ) )
12678, 80, 83, 86, 94, 100, 121, 125climsqz2 12398 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  ~~>  0 )
127 neg1cn 10031 . . . . . . . . . . . . 13  |-  -u 1  e.  CC
128127a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  -u 1  e.  CC )
129 expcl 11362 . . . . . . . . . . . 12  |-  ( (
-u 1  e.  CC  /\  k  e.  NN0 )  ->  ( -u 1 ^ k )  e.  CC )
130128, 129sylan 458 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  ( -u 1 ^ k )  e.  CC )
13155nncnd 9980 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  CC )
13255nnne0d 10008 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  =/=  0 )
133130, 131, 132divrecd 9757 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( -u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( -u
1 ^ k )  x.  ( 1  / 
( ( 2  x.  k )  +  1 ) ) ) )
134 oveq2 6056 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( -u 1 ^ n )  =  ( -u 1 ^ k ) )
135134, 72oveq12d 6066 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( -u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
136 eqid 2412 . . . . . . . . . . . 12  |-  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )
137 ovex 6073 . . . . . . . . . . . 12  |-  ( (
-u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  e.  _V
138135, 136, 137fvmpt 5773 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
139138adantl 453 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u 1 ^ k )  /  (
( 2  x.  k
)  +  1 ) ) )
14076oveq2d 6064 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( -u 1 ^ k
)  x.  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k ) )  =  ( ( -u
1 ^ k )  x.  ( 1  / 
( ( 2  x.  k )  +  1 ) ) ) )
141133, 139, 1403eqtr4d 2454 . . . . . . . . 9  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u 1 ^ k )  x.  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
) ) )
1421, 3, 31, 77, 126, 141iseralt 12441 . . . . . . . 8  |-  (  T. 
->  seq  0 (  +  ,  ( n  e. 
NN0  |->  ( ( -u
1 ^ n )  /  ( ( 2  x.  n )  +  1 ) ) ) )  e.  dom  ~~>  )
143 climdm 12311 . . . . . . . 8  |-  (  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) )  e.  dom  ~~>  <->  seq  0
(  +  ,  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) )  ~~>  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) ) )
144142, 143sylib 189 . . . . . . 7  |-  (  T. 
->  seq  0 (  +  ,  ( n  e. 
NN0  |->  ( ( -u
1 ^ n )  /  ( ( 2  x.  n )  +  1 ) ) ) )  ~~>  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) ) )
145 fvex 5709 . . . . . . . 8  |-  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) )  e.  _V
146136, 20, 145leibpilem2 20742 . . . . . . 7  |-  (  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) )  ~~>  (  ~~>  `  seq  0
(  +  ,  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) ) )  <->  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) )  ~~>  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) ) )
147144, 146sylib 189 . . . . . 6  |-  (  T. 
->  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) )  ~~>  (  ~~>  `  seq  0
(  +  ,  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) ) ) )
148 seqex 11288 . . . . . . 7  |-  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) )  e.  _V
149148, 145breldm 5041 . . . . . 6  |-  (  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) )  ~~>  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) )  ->  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) )  e.  dom  ~~>  )
150147, 149syl 16 . . . . 5  |-  (  T. 
->  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) )  e.  dom  ~~>  )
1511, 3, 4, 22, 150isumclim2 12505 . . . 4  |-  (  T. 
->  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) )  ~~> 
sum_ j  e.  NN0  ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j ) )
152 eqid 2412 . . . . . . . 8  |-  ( x  e.  ( 0 [,] 1 )  |->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )  =  ( x  e.  ( 0 [,] 1 ) 
|->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )
15321, 150, 152abelth2 20319 . . . . . . 7  |-  (  T. 
->  ( x  e.  ( 0 [,] 1 ) 
|->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )  e.  ( ( 0 [,] 1 ) -cn-> CC ) )
154 nnrp 10585 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  n  e.  RR+ )
155154adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR+ )
156155rpreccld 10622 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR+ )
157156rpred 10612 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR )
158156rpge0d 10616 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  0  <_  ( 1  /  n
) )
159 nnge1 9990 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  1  <_  n )
160159adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  n )
161 nnre 9971 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  n  e.  RR )
162161adantl 453 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR )
163162recnd 9078 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  CC )
164163mulid1d 9069 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  (
n  x.  1 )  =  n )
165160, 164breqtrrd 4206 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  ( n  x.  1 ) )
1668a1i 11 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  RR )
167 nngt0 9993 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  0  <  n )
168167adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  0  <  n )
169 ledivmul 9847 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  1  e.  RR  /\  (
n  e.  RR  /\  0  <  n ) )  ->  ( ( 1  /  n )  <_ 
1  <->  1  <_  (
n  x.  1 ) ) )
170166, 166, 162, 168, 169syl112anc 1188 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 1  /  n
)  <_  1  <->  1  <_  ( n  x.  1 ) ) )
171165, 170mpbird 224 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  <_  1 )
172 0re 9055 . . . . . . . . . . 11  |-  0  e.  RR
173172, 8elicc2i 10940 . . . . . . . . . 10  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  <->  ( (
1  /  n )  e.  RR  /\  0  <_  ( 1  /  n
)  /\  ( 1  /  n )  <_ 
1 ) )
174157, 158, 171, 173syl3anbrc 1138 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  ( 0 [,] 1 ) )
175 iirev 18915 . . . . . . . . 9  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
176174, 175syl 16 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
177 eqid 2412 . . . . . . . 8  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n
) ) )
178176, 177fmptd 5860 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) : NN --> ( 0 [,] 1
) )
17981a1i 11 . . . . . . . . 9  |-  (  T. 
->  1  e.  CC )
180 nnex 9970 . . . . . . . . . . 11  |-  NN  e.  _V
181180mptex 5933 . . . . . . . . . 10  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  e.  _V
182181a1i 11 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  e.  _V )
18394recnd 9078 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  CC )
18487oveq2d 6064 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  -  ( 1  /  n ) )  =  ( 1  -  ( 1  /  k
) ) )
185 ovex 6073 . . . . . . . . . . . 12  |-  ( 1  -  ( 1  / 
k ) )  e. 
_V
186184, 177, 185fvmpt 5773 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( 1  / 
k ) ) )
18790oveq2d 6064 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `  k ) )  =  ( 1  -  ( 1  / 
k ) ) )
188186, 187eqtr4d 2447 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `
 k ) ) )
189188adantl 453 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `
 k ) ) )
19078, 80, 83, 179, 182, 183, 189climsubc2 12395 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  ( 1  -  0 ) )
19181subid1i 9336 . . . . . . . 8  |-  ( 1  -  0 )  =  1
192190, 191syl6breq 4219 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  1 )
193 1elunit 10980 . . . . . . . 8  |-  1  e.  ( 0 [,] 1
)
194193a1i 11 . . . . . . 7  |-  (  T. 
->  1  e.  (
0 [,] 1 ) )
19578, 80, 153, 178, 192, 194climcncf 18891 . . . . . 6  |-  (  T. 
->  ( ( x  e.  ( 0 [,] 1
)  |->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )  o.  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) )  ~~>  ( ( x  e.  ( 0 [,] 1 )  |->  sum_ j  e.  NN0  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  x.  (
x ^ j ) ) ) `  1
) )
196 eqidd 2413 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) ) )
197 eqidd 2413 . . . . . . . 8  |-  (  T. 
->  ( x  e.  ( 0 [,] 1 ) 
|->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )  =  ( x  e.  ( 0 [,] 1 ) 
|->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) ) )
198 oveq1 6055 . . . . . . . . . 10  |-  ( x  =  ( 1  -  ( 1  /  n
) )  ->  (
x ^ j )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
199198oveq2d 6064 . . . . . . . . 9  |-  ( x  =  ( 1  -  ( 1  /  n
) )  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  x.  (
x ^ j ) )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  x.  ( ( 1  -  ( 1  /  n ) ) ^
j ) ) )
200199sumeq2sdv 12461 . . . . . . . 8  |-  ( x  =  ( 1  -  ( 1  /  n
) )  ->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) )  =  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  x.  ( ( 1  -  ( 1  /  n ) ) ^
j ) ) )
201176, 196, 197, 200fmptco 5868 . . . . . . 7  |-  (  T. 
->  ( ( x  e.  ( 0 [,] 1
)  |->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( x ^ j
) ) )  o.  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) )  =  ( n  e.  NN  |->  sum_ j  e.  NN0  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  x.  (
( 1  -  (
1  /  n ) ) ^ j ) ) ) )
2022a1i 11 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  ZZ )
20311adantll 695 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  (
( k  -  1 )  /  2 )  e.  NN0 )
2049, 203, 12sylancr 645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  RR )
205204recnd 9078 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  CC )
206205adantllr 700 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  e.  CC )
207 resubcl 9329 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
2088, 157, 207sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  RR )
209208ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
210 simplr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN0 )
211209, 210reexpcld 11503 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  RR )
212211recnd 9078 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  CC )
213 nn0cn 10195 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  k  e.  CC )
214213ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  CC )
21514adantll 695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN )
216215nnne0d 10008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  =/=  0
)
217206, 212, 214, 216div12d 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) )  =  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  x.  (
( -u 1 ^ (
( k  -  1 )  /  2 ) )  /  k ) ) )
21816adantll 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  e.  CC )
219212, 218mulcomd 9073 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  x.  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  =  ( ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
220217, 219eqtrd 2444 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) )  =  ( ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
2217, 220sylan2b 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  -.  ( k  =  0  \/  2 
||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) )  =  ( ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
222221ifeq2da 3733 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) ) ) )
223208recnd 9078 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  CC )
224 expcl 11362 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  -  (
1  /  n ) )  e.  CC  /\  k  e.  NN0 )  -> 
( ( 1  -  ( 1  /  n
) ) ^ k
)  e.  CC )
225223, 224sylan 458 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( 1  -  (
1  /  n ) ) ^ k )  e.  CC )
226225mul02d 9228 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
0  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) )  =  0 )
227226ifeq1d 3721 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  ( 0  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) ) ,  ( ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  x.  ( ( 1  -  ( 1  /  n ) ) ^
k ) ) )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) ) ) )
228222, 227eqtr4d 2447 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  if ( ( k  =  0  \/  2  ||  k ) ,  ( 0  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) ,  ( ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) ) ) )
229 oveq1 6055 . . . . . . . . . . . . . . 15  |-  ( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  =  0  ->  ( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  x.  ( ( 1  -  ( 1  /  n ) ) ^
k ) )  =  ( 0  x.  (
( 1  -  (
1  /  n ) ) ^ k ) ) )
230 oveq1 6055 . . . . . . . . . . . . . . 15  |-  ( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  =  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  -> 
( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) )  =  ( ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
)  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) ) )
231229, 230ifsb 3716 . . . . . . . . . . . . . 14  |-  ( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  x.  ( ( 1  -  ( 1  /  n ) ) ^
k ) )  =  if ( ( k  =  0  \/  2 
||  k ) ,  ( 0  x.  (
( 1  -  (
1  /  n ) ) ^ k ) ) ,  ( ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
)  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) ) )
232228, 231syl6eqr 2462 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  ( if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
233 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
234 c0ex 9049 . . . . . . . . . . . . . . 15  |-  0  e.  _V
235 ovex 6073 . . . . . . . . . . . . . . 15  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) )  e.  _V
236234, 235ifex 3765 . . . . . . . . . . . . . 14  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) )  e. 
_V
237 eqid 2412 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) )  =  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
238237fvmpt2 5779 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  e.  _V )  -> 
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) )
239233, 236, 238sylancl 644 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
240 ovex 6073 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  _V
241234, 240ifex 3765 . . . . . . . . . . . . . . 15  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e. 
_V
24220fvmpt2 5779 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN0  /\  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  e.  _V )  -> 
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  k )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) )
243233, 241, 242sylancl 644 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  k )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) )
244243oveq1d 6063 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) )  =  ( if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  x.  ( ( 1  -  ( 1  /  n ) ) ^
k ) ) )
245232, 239, 2443eqtr4d 2454 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
246245ralrimiva 2757 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  A. k  e.  NN0  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 k )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) ) )
247 nfv 1626 . . . . . . . . . . . 12  |-  F/ j ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  ( ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) )
248 nffvmpt1 5703 . . . . . . . . . . . . 13  |-  F/_ k
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )
249 nffvmpt1 5703 . . . . . . . . . . . . . 14  |-  F/_ k
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )
250 nfcv 2548 . . . . . . . . . . . . . 14  |-  F/_ k  x.
251 nfcv 2548 . . . . . . . . . . . . . 14  |-  F/_ k
( ( 1  -  ( 1  /  n
) ) ^ j
)
252249, 250, 251nfov 6071 . . . . . . . . . . . . 13  |-  F/_ k
( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) )
253248, 252nfeq 2555 . . . . . . . . . . . 12  |-  F/ k ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )  =  ( ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  x.  (
( 1  -  (
1  /  n ) ) ^ j ) )
254 fveq2 5695 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j ) )
255 fveq2 5695 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  k )  =  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j ) )
256 oveq2 6056 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( 1  -  (
1  /  n ) ) ^ k )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
257255, 256oveq12d 6066 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  x.  ( ( 1  -  ( 1  /  n ) ) ^
j ) ) )
258254, 257eqeq12d 2426 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  ( ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  k )  x.  (
( 1  -  (
1  /  n ) ) ^ k ) )  <->  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) ) ) )
259247, 253, 258cbvral 2896 . . . . . . . . . . 11  |-  ( A. k  e.  NN0  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 k )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 k )  x.  ( ( 1  -  ( 1  /  n
) ) ^ k
) )  <->  A. j  e.  NN0  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) ) )
260246, 259sylib 189 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  A. j  e.  NN0  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) ) )
261260r19.21bi 2772 . . . . . . . . 9  |-  ( ( (  T.  /\  n  e.  NN )  /\  j  e.  NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )  =  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) ) )
2625a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( k  =  0  \/  2  ||  k ) )  -> 
0  e.  CC )
263211, 215nndivred 10012 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  RR )
264263recnd 9078 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  CC )
265206, 264mulcld 9072 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) )  e.  CC )
2667, 265sylan2b 462 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  -.  ( k  =  0  \/  2 
||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) )  e.  CC )
267262, 266ifclda 3734 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  e.  CC )
268267, 237fmptd 5860 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) : NN0 --> CC )
269268ffvelrnda 5837 . . . . . . . . . 10  |-  ( ( (  T.  /\  n  e.  NN )  /\  j  e.  NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )  e.  CC )
270261, 269eqeltrrd 2487 . . . . . . . . 9  |-  ( ( (  T.  /\  n  e.  NN )  /\  j  e.  NN0 )  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  x.  (
( 1  -  (
1  /  n ) ) ^ j ) )  e.  CC )
271 0nn0 10200 . . . . . . . . . . . 12  |-  0  e.  NN0
272271a1i 11 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  NN0 )
273 0p1e1 10057 . . . . . . . . . . . . 13  |-  ( 0  +  1 )  =  1
274 seqeq1 11289 . . . . . . . . . . . . 13  |-  ( ( 0  +  1 )  =  1  ->  seq  ( 0  +  1 ) (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  =  seq  1 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) ) )
275273, 274ax-mp 8 . . . . . . . . . . . 12  |-  seq  (
0  +  1 ) (  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) )  =  seq  1
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) )
27679a1i 11 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  ZZ )
277 elnnuz 10486 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  <->  j  e.  ( ZZ>= `  1 )
)
278 nnne0 9996 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  k  =/=  0 )
279278neneqd 2591 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN  ->  -.  k  =  0 )
280 biorf 395 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  k  =  0  -> 
( 2  ||  k  <->  ( k  =  0  \/  2  ||  k ) ) )
281279, 280syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  (
2  ||  k  <->  ( k  =  0  \/  2 
||  k ) ) )
282281bicomd 193 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  (
( k  =  0  \/  2  ||  k
)  <->  2  ||  k
) )
283282ifbid 3725 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) )
28495, 236, 238sylancl 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
285234, 235ifex 3765 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) )  e.  _V
286 eqid 2412 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) )  =  ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
287286fvmpt2 5779 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) )  e.  _V )  ->  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) ) `  k
)  =  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) )
288285, 287mpan2 653 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
289283, 284, 2883eqtr4d 2454 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) ) `  k
) )
290289rgen 2739 . . . . . . . . . . . . . . . . . 18  |-  A. k  e.  NN  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 k )  =  ( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )
291290a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  n  e.  NN )  ->  A. k  e.  NN  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 k )  =  ( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k ) )
292 nfv 1626 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )
293 nffvmpt1 5703 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k
( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )
294248, 293nfeq 2555 . . . . . . . . . . . . . . . . . 18  |-  F/ k ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )
295 fveq2 5695 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  (
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j ) )
296254, 295eqeq12d 2426 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  j  ->  (
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  k )  <->  ( (
k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j ) ) )
297292, 294, 296cbvral 2896 . . . . . . . . . . . . . . . . 17  |-  ( A. k  e.  NN  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  k )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) ) `  k
)  <->  A. j  e.  NN  ( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j ) )
298291, 297sylib 189 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  n  e.  NN )  ->  A. j  e.  NN  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j ) )
299298r19.21bi 2772 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  n  e.  NN )  /\  j  e.  NN )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )  =  ( ( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) ) ) `  j
) )
300277, 299sylan2br 463 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  j  e.  ( ZZ>= `  1 )
)  ->  ( (
k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 j )  =  ( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j ) )
301276, 300seqfeq 11311 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  seq  1 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  =  seq  1 (  +  , 
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) ) )
302157, 166, 171abssubge0d 12197 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  =  ( 1  -  (
1  /  n ) ) )
303 ltsubrp 10607 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR+ )  ->  ( 1  -  (
1  /  n ) )  <  1 )
3048, 156, 303sylancr 645 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  <  1 )
305302, 304eqbrtrd 4200 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  <  1 )
306286atantayl2 20739 . . . . . . . . . . . . . 14  |-  ( ( ( 1  -  (
1  /  n ) )  e.  CC  /\  ( abs `  ( 1  -  ( 1  /  n ) ) )  <  1 )  ->  seq  1 (  +  , 
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) )  ~~>  (arctan `  ( 1  -  ( 1  /  n ) ) ) )
307223, 305, 306syl2anc 643 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  seq  1 (  +  , 
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) )  ~~>  (arctan `  ( 1  -  ( 1  /  n ) ) ) )
308301, 307eqbrtrd 4200 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  seq  1 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  ~~>  (arctan `  ( 1  -  (
1  /  n ) ) ) )
309275, 308syl5eqbr 4213 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  seq  ( 0  +  1 ) (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  ~~>  (arctan `  ( 1  -  (
1  /  n ) ) ) )
3101, 272, 269, 309clim2ser2 12412 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  ~~>  ( (arctan `  ( 1  -  (
1  /  n ) ) )  +  (  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) ) `
 0 ) ) )
311 seq1 11299 . . . . . . . . . . . . . 14  |-  ( 0  e.  ZZ  ->  (  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) ) `  0
)  =  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 0 ) )
3122, 311ax-mp 8 . . . . . . . . . . . . 13  |-  (  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) ) `  0
)  =  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 0 )
313 iftrue 3713 . . . . . . . . . . . . . . . 16  |-  ( ( k  =  0  \/  2  ||  k )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) )  =  0 )
314313orcs 384 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  0 )
315314, 237, 234fvmpt 5773 . . . . . . . . . . . . . 14  |-  ( 0  e.  NN0  ->  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 0 )  =  0 )
316271, 315ax-mp 8 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) `
 0 )  =  0
317312, 316eqtri 2432 . . . . . . . . . . . 12  |-  (  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) ) `  0
)  =  0
318317oveq2i 6059 . . . . . . . . . . 11  |-  ( (arctan `  ( 1  -  (
1  /  n ) ) )  +  (  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) ) `
 0 ) )  =  ( (arctan `  ( 1  -  (
1  /  n ) ) )  +  0 )
319 atanrecl 20712 . . . . . . . . . . . . . 14  |-  ( ( 1  -  ( 1  /  n ) )  e.  RR  ->  (arctan `  ( 1  -  (
1  /  n ) ) )  e.  RR )
320208, 319syl 16 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  (arctan `  ( 1  -  (
1  /  n ) ) )  e.  RR )
321320recnd 9078 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  (arctan `  ( 1  -  (
1  /  n ) ) )  e.  CC )
322321addid1d 9230 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
(arctan `  ( 1  -  ( 1  /  n ) ) )  +  0 )  =  (arctan `  ( 1  -  ( 1  /  n ) ) ) )
323318, 322syl5eq 2456 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
(arctan `  ( 1  -  ( 1  /  n ) ) )  +  (  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) ) ) ) `  0 ) )  =  (arctan `  ( 1  -  (
1  /  n ) ) ) )
324310, 323breqtrd 4204 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) )  ~~>  (arctan `  ( 1  -  (
1  /  n ) ) ) )
3251, 202, 261, 270, 324isumclim 12504 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  sum_ j  e.  NN0  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||