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

Theorem leibpi 20238
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 12157). (2) Using leibpilem2 20237 to rewrite the series as a power series, it is the  x  =  1 special case of the Taylor series for arctan (atantayl2 20234). (3) Although we cannot directly plug  x  =  1 into atantayl2 20234, Abel's theorem (abelth2 19818) 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 20232) 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 10262 . . . . 5  |-  NN0  =  ( ZZ>= `  0 )
2 0z 10035 . . . . . 6  |-  0  e.  ZZ
32a1i 10 . . . . 5  |-  (  T. 
->  0  e.  ZZ )
4 eqidd 2284 . . . . 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 8831 . . . . . . . . . 10  |-  0  e.  CC
65a1i 10 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  ( k  =  0  \/  2  ||  k
) )  ->  0  e.  CC )
7 ioran 476 . . . . . . . . . 10  |-  ( -.  ( k  =  0  \/  2  ||  k
)  <->  ( -.  k  =  0  /\  -.  2  ||  k ) )
8 1re 8837 . . . . . . . . . . . . . 14  |-  1  e.  RR
98renegcli 9108 . . . . . . . . . . . . 13  |-  -u 1  e.  RR
10 leibpilem1 20236 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( k  e.  NN  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )
)
1110simprd 449 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( k  - 
1 )  /  2
)  e.  NN0 )
12 reexpcl 11120 . . . . . . . . . . . . 13  |-  ( (
-u 1  e.  RR  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  e.  RR )
139, 11, 12sylancr 644 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( -u 1 ^ (
( k  -  1 )  /  2 ) )  e.  RR )
1410simpld 445 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
k  e.  NN )
1513, 14nndivred 9794 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  RR )
1615recnd 8861 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  CC )
177, 16sylan2b 461 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  -.  ( k  =  0  \/  2  ||  k
) )  ->  (
( -u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  CC )
186, 17ifclda 3592 . . . . . . . 8  |-  ( k  e.  NN0  ->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e.  CC )
1918adantl 452 . . . . . . 7  |-  ( (  T.  /\  k  e. 
NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  e.  CC )
20 eqid 2283 . . . . . . 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 5684 . . . . . 6  |-  (  T. 
->  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) : NN0 --> CC )
22 ffvelrn 5663 . . . . . 6  |-  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) : NN0 --> CC  /\  j  e.  NN0 )  -> 
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )  e.  CC )
2321, 22sylan 457 . . . . 5  |-  ( (  T.  /\  j  e. 
NN0 )  ->  (
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) `  j )  e.  CC )
24 2nn0 9982 . . . . . . . . . . . . . 14  |-  2  e.  NN0
2524a1i 10 . . . . . . . . . . . . 13  |-  (  T. 
->  2  e.  NN0 )
26 nn0mulcl 10000 . . . . . . . . . . . . 13  |-  ( ( 2  e.  NN0  /\  n  e.  NN0 )  -> 
( 2  x.  n
)  e.  NN0 )
2725, 26sylan 457 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
2  x.  n )  e.  NN0 )
28 nn0p1nn 10003 . . . . . . . . . . . 12  |-  ( ( 2  x.  n )  e.  NN0  ->  ( ( 2  x.  n )  +  1 )  e.  NN )
2927, 28syl 15 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
3029nnrecred 9791 . . . . . . . . . 10  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  e.  RR )
31 eqid 2283 . . . . . . . . . 10  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) )
3230, 31fmptd 5684 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) : NN0 --> RR )
33 nn0mulcl 10000 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  k  e.  NN0 )  -> 
( 2  x.  k
)  e.  NN0 )
3425, 33sylan 457 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  NN0 )
3534nn0red 10019 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  RR )
36 peano2nn0 10004 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
3736adantl 452 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  NN0 )
38 nn0mulcl 10000 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  ( k  +  1 )  e.  NN0 )  ->  ( 2  x.  (
k  +  1 ) )  e.  NN0 )
3924, 37, 38sylancr 644 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  NN0 )
4039nn0red 10019 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  RR )
418a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  1  e.  RR )
42 nn0re 9974 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  k  e.  RR )
4342adantl 452 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  e.  RR )
4443lep1d 9688 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  <_  ( k  +  1 ) )
45 peano2re 8985 . . . . . . . . . . . . . . 15  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
4643, 45syl 15 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  RR )
47 2re 9815 . . . . . . . . . . . . . . 15  |-  2  e.  RR
4847a1i 10 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  2  e.  RR )
49 2pos 9828 . . . . . . . . . . . . . . 15  |-  0  <  2
5049a1i 10 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  2 )
51 lemul2 9609 . . . . . . . . . . . . . 14  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( k  <_  ( k  +  1 )  <->  ( 2  x.  k )  <_  (
2  x.  ( k  +  1 ) ) ) )
5243, 46, 48, 50, 51syl112anc 1186 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  <_  ( k  +  1 )  <->  ( 2  x.  k )  <_ 
( 2  x.  (
k  +  1 ) ) ) )
5344, 52mpbid 201 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  <_  ( 2  x.  ( k  +  1 ) ) )
5435, 40, 41, 53leadd1dd 9386 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  <_  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
55 nn0p1nn 10003 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
5634, 55syl 15 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
5756nnred 9761 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
5856nngt0d 9789 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
59 nn0p1nn 10003 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  ( k  +  1 ) )  e.  NN0  ->  ( ( 2  x.  ( k  +  1 ) )  +  1 )  e.  NN )
6039, 59syl 15 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  NN )
6160nnred 9761 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  RR )
6260nngt0d 9789 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
63 lerec 9638 . . . . . . . . . . . 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 ) ) ) )
6457, 58, 61, 62, 63syl22anc 1183 . . . . . . . . . . 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 ) ) ) )
6554, 64mpbid 201 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  <_  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
66 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( n  =  ( k  +  1 )  ->  (
2  x.  n )  =  ( 2  x.  ( k  +  1 ) ) )
6766oveq1d 5873 . . . . . . . . . . . . 13  |-  ( n  =  ( k  +  1 )  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
6867oveq2d 5874 . . . . . . . . . . . 12  |-  ( n  =  ( k  +  1 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
69 ovex 5883 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  e. 
_V
7068, 31, 69fvmpt 5602 . . . . . . . . . . 11  |-  ( ( k  +  1 )  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 ( k  +  1 ) )  =  ( 1  /  (
( 2  x.  (
k  +  1 ) )  +  1 ) ) )
7137, 70syl 15 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  (
k  +  1 ) )  =  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
72 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
7372oveq1d 5873 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  k )  +  1 ) )
7473oveq2d 5874 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
75 ovex 5883 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  k )  +  1 ) )  e. 
_V
7674, 31, 75fvmpt 5602 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k )  =  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
7776adantl 452 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
7865, 71, 773brtr4d 4053 . . . . . . . . 9  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  (
k  +  1 ) )  <_  ( (
n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k ) )
79 nnuz 10263 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
80 1z 10053 . . . . . . . . . . 11  |-  1  e.  ZZ
8180a1i 10 . . . . . . . . . 10  |-  (  T. 
->  1  e.  ZZ )
82 ax-1cn 8795 . . . . . . . . . . 11  |-  1  e.  CC
83 divcnv 12312 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  (
n  e.  NN  |->  ( 1  /  n ) )  ~~>  0 )
8482, 83mp1i 11 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  /  n
) )  ~~>  0 )
85 nn0ex 9971 . . . . . . . . . . . 12  |-  NN0  e.  _V
8685mptex 5746 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  e.  _V
8786a1i 10 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  e.  _V )
88 oveq2 5866 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
1  /  n )  =  ( 1  / 
k ) )
89 eqid 2283 . . . . . . . . . . . . 13  |-  ( n  e.  NN  |->  ( 1  /  n ) )  =  ( n  e.  NN  |->  ( 1  /  n ) )
90 ovex 5883 . . . . . . . . . . . . 13  |-  ( 1  /  k )  e. 
_V
9188, 89, 90fvmpt 5602 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
9291adantl 452 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
93 nnrecre 9782 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
9493adantl 452 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  k )  e.  RR )
9592, 94eqeltrd 2357 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  RR )
96 nnnn0 9972 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  NN0 )
9796adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  NN0 )
9897, 76syl 15 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
9996, 56sylan2 460 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
10099nnrecred 9791 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR )
10198, 100eqeltrd 2357 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  e.  RR )
102 nnre 9753 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  k  e.  RR )
103102adantl 452 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  RR )
10424, 97, 33sylancr 644 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  NN0 )
105104nn0red 10019 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  RR )
106 peano2re 8985 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  RR  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
107105, 106syl 15 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
108 nn0addge1 10010 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  RR  /\  k  e.  NN0 )  -> 
k  <_  ( k  +  k ) )
109103, 97, 108syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( k  +  k ) )
110103recnd 8861 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  CC )
1111102timesd 9954 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  =  ( k  +  k ) )
112109, 111breqtrrd 4049 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( 2  x.  k
) )
113105lep1d 9688 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  <_  ( ( 2  x.  k )  +  1 ) )
114103, 105, 107, 112, 113letrd 8973 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( ( 2  x.  k )  +  1 ) )
115 nngt0 9775 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  0  <  k )
116115adantl 452 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  k )
11799nnred 9761 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
11899nngt0d 9789 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
119 lerec 9638 . . . . . . . . . . . . 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 ) ) )
120103, 116, 117, 118, 119syl22anc 1183 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
k  <_  ( (
2  x.  k )  +  1 )  <->  ( 1  /  ( ( 2  x.  k )  +  1 ) )  <_ 
( 1  /  k
) ) )
121114, 120mpbid 201 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  <_  ( 1  / 
k ) )
122121, 98, 923brtr4d 4053 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  <_  ( (
n  e.  NN  |->  ( 1  /  n ) ) `  k ) )
12399nnrpd 10389 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR+ )
124123rpreccld 10400 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR+ )
125124rpge0d 10394 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
126125, 98breqtrrd 4049 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) ) `  k ) )
12779, 81, 84, 87, 95, 101, 122, 126climsqz2 12115 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  ~~>  0 )
128 neg1cn 9813 . . . . . . . . . . . . 13  |-  -u 1  e.  CC
129128a1i 10 . . . . . . . . . . . 12  |-  (  T. 
->  -u 1  e.  CC )
130 expcl 11121 . . . . . . . . . . . 12  |-  ( (
-u 1  e.  CC  /\  k  e.  NN0 )  ->  ( -u 1 ^ k )  e.  CC )
131129, 130sylan 457 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  ( -u 1 ^ k )  e.  CC )
13256nncnd 9762 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  CC )
13356nnne0d 9790 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  =/=  0 )
134131, 132, 133divrecd 9539 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( -u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( -u
1 ^ k )  x.  ( 1  / 
( ( 2  x.  k )  +  1 ) ) ) )
135 oveq2 5866 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( -u 1 ^ n )  =  ( -u 1 ^ k ) )
136135, 73oveq12d 5876 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( -u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
137 eqid 2283 . . . . . . . . . . . 12  |-  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )
138 ovex 5883 . . . . . . . . . . . 12  |-  ( (
-u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  e.  _V
139136, 137, 138fvmpt 5602 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
140139adantl 452 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u 1 ^ k )  /  (
( 2  x.  k
)  +  1 ) ) )
14177oveq2d 5874 . . . . . . . . . 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 ) ) ) )
142134, 140, 1413eqtr4d 2325 . . . . . . . . 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
) ) )
1431, 3, 32, 78, 127, 142iseralt 12157 . . . . . . . 8  |-  (  T. 
->  seq  0 (  +  ,  ( n  e. 
NN0  |->  ( ( -u
1 ^ n )  /  ( ( 2  x.  n )  +  1 ) ) ) )  e.  dom  ~~>  )
144 climdm 12028 . . . . . . . 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 ) ) ) ) ) )
145143, 144sylib 188 . . . . . . 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 ) ) ) ) ) )
146 fvex 5539 . . . . . . . 8  |-  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) )  e.  _V
147137, 20, 146leibpilem2 20237 . . . . . . 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 ) ) ) ) ) )
148145, 147sylib 188 . . . . . 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 ) ) ) ) ) )
149 seqex 11048 . . . . . . 7  |-  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) )  e.  _V
150149, 146breldm 4883 . . . . . 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  ~~>  )
151148, 150syl 15 . . . . 5  |-  (  T. 
->  seq  0 (  +  ,  ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) )  e.  dom  ~~>  )
1521, 3, 4, 23, 151isumclim2 12221 . . . 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 ) )
153 eqid 2283 . . . . . . . 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
) ) )
15421, 151, 153abelth2 19818 . . . . . . 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 ) )
155 nnrp 10363 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  n  e.  RR+ )
156155adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR+ )
157156rpreccld 10400 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR+ )
158157rpred 10390 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR )
159157rpge0d 10394 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  0  <_  ( 1  /  n
) )
160 nnge1 9772 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  1  <_  n )
161160adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  n )
162 nnre 9753 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  n  e.  RR )
163162adantl 452 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR )
164163recnd 8861 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  CC )
165164mulid1d 8852 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  (
n  x.  1 )  =  n )
166161, 165breqtrrd 4049 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  ( n  x.  1 ) )
1678a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  RR )
168 nngt0 9775 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  0  <  n )
169168adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  0  <  n )
170 ledivmul 9629 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  1  e.  RR  /\  (
n  e.  RR  /\  0  <  n ) )  ->  ( ( 1  /  n )  <_ 
1  <->  1  <_  (
n  x.  1 ) ) )
171167, 167, 163, 169, 170syl112anc 1186 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 1  /  n
)  <_  1  <->  1  <_  ( n  x.  1 ) ) )
172166, 171mpbird 223 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  <_  1 )
173 0re 8838 . . . . . . . . . . 11  |-  0  e.  RR
174173, 8elicc2i 10716 . . . . . . . . . 10  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  <->  ( (
1  /  n )  e.  RR  /\  0  <_  ( 1  /  n
)  /\  ( 1  /  n )  <_ 
1 ) )
175158, 159, 172, 174syl3anbrc 1136 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  ( 0 [,] 1 ) )
176 iirev 18427 . . . . . . . . 9  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
177175, 176syl 15 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
178 eqid 2283 . . . . . . . 8  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n
) ) )
179177, 178fmptd 5684 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) : NN --> ( 0 [,] 1
) )
18082a1i 10 . . . . . . . . 9  |-  (  T. 
->  1  e.  CC )
181 nnex 9752 . . . . . . . . . . 11  |-  NN  e.  _V
182181mptex 5746 . . . . . . . . . 10  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  e.  _V
183182a1i 10 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  e.  _V )
18495recnd 8861 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  CC )
18588oveq2d 5874 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  -  ( 1  /  n ) )  =  ( 1  -  ( 1  /  k
) ) )
186 ovex 5883 . . . . . . . . . . . 12  |-  ( 1  -  ( 1  / 
k ) )  e. 
_V
187185, 178, 186fvmpt 5602 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( 1  / 
k ) ) )
18891oveq2d 5874 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `  k ) )  =  ( 1  -  ( 1  / 
k ) ) )
189187, 188eqtr4d 2318 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `
 k ) ) )
190189adantl 452 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `
 k ) ) )
19179, 81, 84, 180, 183, 184, 190climsubc2 12112 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  ( 1  -  0 ) )
19282subid1i 9118 . . . . . . . 8  |-  ( 1  -  0 )  =  1
193191, 192syl6breq 4062 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  1 )
194 1elunit 10755 . . . . . . . 8  |-  1  e.  ( 0 [,] 1
)
195194a1i 10 . . . . . . 7  |-  (  T. 
->  1  e.  (
0 [,] 1 ) )
19679, 81, 154, 179, 193, 195climcncf 18404 . . . . . 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
) )
197 eqidd 2284 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) ) )
198 eqidd 2284 . . . . . . . 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
) ) ) )
199 oveq1 5865 . . . . . . . . . 10  |-  ( x  =  ( 1  -  ( 1  /  n
) )  ->  (
x ^ j )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
200199oveq2d 5874 . . . . . . . . 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 ) ) )
201200sumeq2sdv 12177 . . . . . . . 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 ) ) )
202177, 197, 198, 201fmptco 5691 . . . . . . 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 ) ) ) )
2032a1i 10 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  ZZ )
20411adantll 694 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  (
( k  -  1 )  /  2 )  e.  NN0 )
2059, 204, 12sylancr 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  RR )
206205recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  CC )
207206adantllr 699 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  e.  CC )
208 resubcl 9111 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
2098, 158, 208sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  RR )
210209ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
211 simplr 731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN0 )
212210, 211reexpcld 11262 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  RR )
213212recnd 8861 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  CC )
214 nn0cn 9975 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  k  e.  CC )
215214ad2antlr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  CC )
21614adantll 694 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN )
217216nnne0d 9790 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  =/=  0
)
218207, 213, 215, 217div12d 9572 . . . . . . . . . . . . . . . . . 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 ) ) )
21916adantll 694 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  e.  CC )
220213, 219mulcomd 8856 . . . . . . . . . . . . . . . . . 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
) ) )
221218, 220eqtrd 2315 . . . . . . . . . . . . . . . . 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
) ) )
2227, 221sylan2b 461 . . . . . . . . . . . . . . . 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
) ) )
223222ifeq2da 3591 . . . . . . . . . . . . . . 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 ) ) ) )
224209recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  CC )
225 expcl 11121 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  -  (
1  /  n ) )  e.  CC  /\  k  e.  NN0 )  -> 
( ( 1  -  ( 1  /  n
) ) ^ k
)  e.  CC )
226224, 225sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( 1  -  (
1  /  n ) ) ^ k )  e.  CC )
227226mul02d 9010 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
0  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) )  =  0 )
228227ifeq1d 3579 . . . . . . . . . . . . . . 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 ) ) ) )
229223, 228eqtr4d 2318 . . . . . . . . . . . . . 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 ) ) ) )
230 oveq1 5865 . . . . . . . . . . . . . . 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 ) ) )
231 oveq1 5865 . . . . . . . . . . . . . . 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 ) ) )
232230, 231ifsb 3574 . . . . . . . . . . . . . 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 ) ) )
233229, 232syl6eqr 2333 . . . . . . . . . . . . 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
) ) )
234 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
235 c0ex 8832 . . . . . . . . . . . . . . 15  |-  0  e.  _V
236 ovex 5883 . . . . . . . . . . . . . . 15  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) )  e.  _V
237235, 236ifex 3623 . . . . . . . . . . . . . 14  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) )  e. 
_V
238 eqid 2283 . . . . . . . . . . . . . . 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 ) ) ) )
239238fvmpt2 5608 . . . . . . . . . . . . . 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 ) ) ) )
240234, 237, 239sylancl 643 . . . . . . . . . . . . 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 ) ) ) )
241 ovex 5883 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  _V
242235, 241ifex 3623 . . . . . . . . . . . . . . 15  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e. 
_V
24320fvmpt2 5608 . . . . . . . . . . . . . . 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 ) ) )
244234, 242, 243sylancl 643 . . . . . . . . . . . . . 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
) ) )
245244oveq1d 5873 . . . . . . . . . . . . 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 ) ) )
246233, 240, 2453eqtr4d 2325 . . . . . . . . . . . 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
) ) )
247246ralrimiva 2626 . . . . . . . . . . 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
) ) )
248 nfv 1605 . . . . . . . . . . . 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 ) )
249 nfmpt1 4109 . . . . . . . . . . . . . 14  |-  F/_ k
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) )
250 nfcv 2419 . . . . . . . . . . . . . 14  |-  F/_ k
j
251249, 250nffv 5532 . . . . . . . . . . . . 13  |-  F/_ k
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) ) `  j )
252 nfmpt1 4109 . . . . . . . . . . . . . . 15  |-  F/_ k
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) )
253252, 250nffv 5532 . . . . . . . . . . . . . 14  |-  F/_ k
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )
254 nfcv 2419 . . . . . . . . . . . . . 14  |-  F/_ k  x.
255 nfcv 2419 . . . . . . . . . . . . . 14  |-  F/_ k
( ( 1  -  ( 1  /  n
) ) ^ j
)
256253, 254, 255nfov 5881 . . . . . . . . . . . . 13  |-  F/_ k
( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) `
 j )  x.  ( ( 1  -  ( 1  /  n
) ) ^ j
) )
257251, 256nfeq 2426 . . . . . . . . . . . 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 ) )
258 fveq2 5525 . . . . . . . . . . . . 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 ) )
259 fveq2 5525 . . . . . . . . . . . . . 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 ) )
260 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( 1  -  (
1  /  n ) ) ^ k )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
261259, 260oveq12d 5876 . . . . . . . . . . . . 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 ) ) )
262258, 261eqeq12d 2297 . . . . . . . . . . . 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
) ) ) )
263248, 257, 262cbvral 2760 . . . . . . . . . . 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
) ) )
264247, 263sylib 188 . . . . . . . . . 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
) ) )
265264r19.21bi 2641 . . . . . . . . 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
) ) )
2665a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( k  =  0  \/  2  ||  k ) )  -> 
0  e.  CC )
267212, 216nndivred 9794 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  RR )
268267recnd 8861 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  CC )
269207, 268mulcld 8855 . . . . . . . . . . . . . 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 )
2707, 269sylan2b 461 . . . . . . . . . . . . 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 )
271266, 270ifclda 3592 . . . . . . . . . . . 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 )
272271, 238fmptd 5684 . . . . . . . . . . 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 )
273 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) : NN0 --> CC  /\  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 )
274272, 273sylan 457 . . . . . . . . . 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 )
275265, 274eqeltrrd 2358 . . . . . . . . 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 )
276 0nn0 9980 . . . . . . . . . . . 12  |-  0  e.  NN0
277276a1i 10 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  NN0 )
278 0p1e1 9839 . . . . . . . . . . . . 13  |-  ( 0  +  1 )  =  1
279 seqeq1 11049 . . . . . . . . . . . . 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 ) ) ) ) ) )
280278, 279ax-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
) ) ) ) )
28180a1i 10 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  ZZ )
282 elnnuz 10264 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  <->  j  e.  ( ZZ>= `  1 )
)
283 nnne0 9778 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  k  =/=  0 )
284283neneqd 2462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN  ->  -.  k  =  0 )
285 biorf 394 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  k  =  0  -> 
( 2  ||  k  <->  ( k  =  0  \/  2  ||  k ) ) )
286284, 285syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  (
2  ||  k  <->  ( k  =  0  \/  2 
||  k ) ) )
287286bicomd 192 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  (
( k  =  0  \/  2  ||  k
)  <->  2  ||  k
) )
288287ifbid 3583 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
28996, 237, 239sylancl 643 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
290235, 236ifex 3623 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) )  e.  _V
291 eqid 2283 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
292291fvmpt2 5608 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
293290, 292mpan2 652 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
294288, 289, 2933eqtr4d 2325 . . . . . . . . . . . . . . . . . . 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
) )
295294rgen 2608 . . . . . . . . . . . . . . . . . 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 )
296295a1i 10 . . . . . . . . . . . . . . . . 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 ) )
297 nfv 1605 . . . . . . . . . . . . . . . . . 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 )
298 nfmpt1 4109 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
299298, 250nffv 5532 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k
( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )
300251, 299nfeq 2426 . . . . . . . . . . . . . . . . . 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 )
301 fveq2 5525 . . . . . . . . . . . . . . . . . . 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 ) )
302258, 301eqeq12d 2297 . . . . . . . . . . . . . . . . . 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 ) ) )
303297, 300, 302cbvral 2760 . . . . . . . . . . . . . . . . 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 ) )
304296, 303sylib 188 . . . . . . . . . . . . . . . 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 ) )
305304r19.21bi 2641 . . . . . . . . . . . . . . 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
) )
306282, 305sylan2br 462 . . . . . . . . . . . . . 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 ) )
307281, 306seqfeq 11071 . . . . . . . . . . . . 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 ) ) ) ) ) )
308158, 167, 172abssubge0d 11914 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  =  ( 1  -  (
1  /  n ) ) )
309 ltsubrp 10385 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR+ )  ->  ( 1  -  (
1  /  n ) )  <  1 )
3108, 157, 309sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  <  1 )
311308, 310eqbrtrd 4043 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  <  1 )
312291atantayl2 20234 . . . . . . . . . . . . . 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 ) ) ) )
313224, 311, 312syl2anc 642 . . . . . . . . . . . . 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 ) ) ) )
314307, 313eqbrtrd 4043 . . . . . . . . . . . 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 ) ) ) )
315280, 314syl5eqbr 4056 . . . . . . . . . . 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 ) ) ) )
3161, 277, 274, 315clim2ser2 12129 . . . . . . . . . 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 ) ) )
317 seq1 11059 . . . . . . . . . . . . . 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 ) )
3182, 317ax-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 )
319 iftrue 3571 . . . . . . . . . . . . . . . 16  |-  ( ( k  =  0  \/  2  ||  k )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) )  =  0 )
320319orcs 383 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  0 )
321320, 238, 235fvmpt 5602 . . . . . . . . . . . . . 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 )
322276, 321ax-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
323318, 322eqtri 2303 . . . . . . . . . . . 12  |-  (  seq  0 (  +  ,