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

Theorem leibpi 20186
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 12108). (2) Using leibpilem2 20185 to rewrite the series as a power series, it is the  x  =  1 special case of the Taylor series for arctan (atantayl2 20182). (3) Although we cannot directly plug  x  =  1 into atantayl2 20182, Abel's theorem (abelth2 19766) 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 20180) 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
StepHypRef Expression
1 nn0uz 10215 . . . . 5  |-  NN0  =  ( ZZ>= `  0 )
2 0z 9988 . . . . . 6  |-  0  e.  ZZ
32a1i 12 . . . . 5  |-  (  T. 
->  0  e.  ZZ )
4 eqidd 2257 . . . . 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 8785 . . . . . . . . . 10  |-  0  e.  CC
65a1i 12 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  ( k  =  0  \/  2  ||  k
) )  ->  0  e.  CC )
7 ioran 478 . . . . . . . . . 10  |-  ( -.  ( k  =  0  \/  2  ||  k
)  <->  ( -.  k  =  0  /\  -.  2  ||  k ) )
8 1re 8791 . . . . . . . . . . . . . 14  |-  1  e.  RR
98renegcli 9062 . . . . . . . . . . . . 13  |-  -u 1  e.  RR
10 leibpilem1 20184 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( k  e.  NN  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )
)
1110simprd 451 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( k  - 
1 )  /  2
)  e.  NN0 )
12 reexpcl 11072 . . . . . . . . . . . . 13  |-  ( (
-u 1  e.  RR  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  e.  RR )
139, 11, 12sylancr 647 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( -u 1 ^ (
( k  -  1 )  /  2 ) )  e.  RR )
1410simpld 447 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
k  e.  NN )
1513, 14nndivred 9748 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  RR )
1615recnd 8815 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  ( -.  k  = 
0  /\  -.  2  ||  k ) )  -> 
( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k )  e.  CC )
177, 16sylan2b 463 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  -.  ( k  =  0  \/  2  ||  k
) )  ->  (
( -u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  CC )
186, 17ifclda 3552 . . . . . . . 8  |-  ( k  e.  NN0  ->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e.  CC )
1918adantl 454 . . . . . . 7  |-  ( (  T.  /\  k  e. 
NN0 )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) )  e.  CC )
20 eqid 2256 . . . . . . 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 5604 . . . . . 6  |-  (  T. 
->  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) ) : NN0 --> CC )
22 ffvelrn 5583 . . . . . 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 459 . . . . 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 9935 . . . . . . . . . . . . . 14  |-  2  e.  NN0
2524a1i 12 . . . . . . . . . . . . 13  |-  (  T. 
->  2  e.  NN0 )
26 nn0mulcl 9953 . . . . . . . . . . . . 13  |-  ( ( 2  e.  NN0  /\  n  e.  NN0 )  -> 
( 2  x.  n
)  e.  NN0 )
2725, 26sylan 459 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
2  x.  n )  e.  NN0 )
28 nn0p1nn 9956 . . . . . . . . . . . 12  |-  ( ( 2  x.  n )  e.  NN0  ->  ( ( 2  x.  n )  +  1 )  e.  NN )
2927, 28syl 17 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
3029nnrecred 9745 . . . . . . . . . 10  |-  ( (  T.  /\  n  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  e.  RR )
31 eqid 2256 . . . . . . . . . 10  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) )
3230, 31fmptd 5604 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) : NN0 --> RR )
33 nn0mulcl 9953 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  k  e.  NN0 )  -> 
( 2  x.  k
)  e.  NN0 )
3425, 33sylan 459 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  NN0 )
3534nn0red 9972 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  e.  RR )
36 peano2nn0 9957 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
3736adantl 454 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  NN0 )
38 nn0mulcl 9953 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN0  /\  ( k  +  1 )  e.  NN0 )  ->  ( 2  x.  (
k  +  1 ) )  e.  NN0 )
3924, 37, 38sylancr 647 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  NN0 )
4039nn0red 9972 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  ( k  +  1 ) )  e.  RR )
418a1i 12 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  1  e.  RR )
42 nn0re 9927 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  k  e.  RR )
4342adantl 454 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  e.  RR )
4443lep1d 9642 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  k  <_  ( k  +  1 ) )
45 peano2re 8939 . . . . . . . . . . . . . . 15  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
4643, 45syl 17 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  +  1 )  e.  RR )
47 2re 9769 . . . . . . . . . . . . . . 15  |-  2  e.  RR
4847a1i 12 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  2  e.  RR )
49 2pos 9782 . . . . . . . . . . . . . . 15  |-  0  <  2
5049a1i 12 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  2 )
51 lemul2 9563 . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
k  <_  ( k  +  1 )  <->  ( 2  x.  k )  <_ 
( 2  x.  (
k  +  1 ) ) ) )
5344, 52mpbid 203 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
2  x.  k )  <_  ( 2  x.  ( k  +  1 ) ) )
5435, 40, 41, 53leadd1dd 9340 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  <_  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
55 nn0p1nn 9956 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
5634, 55syl 17 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
5756nnred 9715 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
5856nngt0d 9743 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
59 nn0p1nn 9956 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  ( k  +  1 ) )  e.  NN0  ->  ( ( 2  x.  ( k  +  1 ) )  +  1 )  e.  NN )
6039, 59syl 17 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  NN )
6160nnred 9715 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  (
k  +  1 ) )  +  1 )  e.  RR )
6260nngt0d 9743 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e. 
NN0 )  ->  0  <  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
63 lerec 9592 . . . . . . . . . . . 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 1188 . . . . . . . . . . 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 203 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  <_  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
66 oveq2 5786 . . . . . . . . . . . . . 14  |-  ( n  =  ( k  +  1 )  ->  (
2  x.  n )  =  ( 2  x.  ( k  +  1 ) ) )
6766oveq1d 5793 . . . . . . . . . . . . 13  |-  ( n  =  ( k  +  1 )  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
6867oveq2d 5794 . . . . . . . . . . . 12  |-  ( n  =  ( k  +  1 )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
69 ovex 5803 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )  e. 
_V
7068, 31, 69fvmpt 5522 . . . . . . . . . . 11  |-  ( ( k  +  1 )  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 ( k  +  1 ) )  =  ( 1  /  (
( 2  x.  (
k  +  1 ) )  +  1 ) ) )
7137, 70syl 17 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  (
k  +  1 ) )  =  ( 1  /  ( ( 2  x.  ( k  +  1 ) )  +  1 ) ) )
72 oveq2 5786 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
2  x.  n )  =  ( 2  x.  k ) )
7372oveq1d 5793 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
( 2  x.  n
)  +  1 )  =  ( ( 2  x.  k )  +  1 ) )
7473oveq2d 5794 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  =  ( 1  / 
( ( 2  x.  k )  +  1 ) ) )
75 ovex 5803 . . . . . . . . . . . 12  |-  ( 1  /  ( ( 2  x.  k )  +  1 ) )  e. 
_V
7674, 31, 75fvmpt 5522 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) ) `
 k )  =  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
7776adantl 454 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
7865, 71, 773brtr4d 4013 . . . . . . . . 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 10216 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
80 1z 10006 . . . . . . . . . . 11  |-  1  e.  ZZ
8180a1i 12 . . . . . . . . . 10  |-  (  T. 
->  1  e.  ZZ )
82 ax-1cn 8749 . . . . . . . . . . 11  |-  1  e.  CC
83 divcnv 12260 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  (
n  e.  NN  |->  ( 1  /  n ) )  ~~>  0 )
8482, 83mp1i 13 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  /  n
) )  ~~>  0 )
85 nn0ex 9924 . . . . . . . . . . . 12  |-  NN0  e.  _V
8685mptex 5666 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )  e.  _V
8786a1i 12 . . . . . . . . . 10  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  e.  _V )
88 oveq2 5786 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
1  /  n )  =  ( 1  / 
k ) )
89 eqid 2256 . . . . . . . . . . . . 13  |-  ( n  e.  NN  |->  ( 1  /  n ) )  =  ( n  e.  NN  |->  ( 1  /  n ) )
90 ovex 5803 . . . . . . . . . . . . 13  |-  ( 1  /  k )  e. 
_V
9188, 89, 90fvmpt 5522 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
9291adantl 454 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  =  ( 1  /  k ) )
93 nnrecre 9736 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
9493adantl 454 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  k )  e.  RR )
9592, 94eqeltrd 2330 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  RR )
96 nnnn0 9925 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  NN0 )
9796adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  NN0 )
9897, 76syl 17 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
9996, 56sylan2 462 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  NN )
10099nnrecred 9745 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR )
10198, 100eqeltrd 2330 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  e.  RR )
102 nnre 9707 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  k  e.  RR )
103102adantl 454 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  RR )
10424, 97, 33sylancr 647 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  NN0 )
105104nn0red 9972 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  e.  RR )
106 peano2re 8939 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  k )  e.  RR  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
107105, 106syl 17 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
108 nn0addge1 9963 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  RR  /\  k  e.  NN0 )  -> 
k  <_  ( k  +  k ) )
109103, 97, 108syl2anc 645 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( k  +  k ) )
110103recnd 8815 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  k  e.  CC )
1111102timesd 9907 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  =  ( k  +  k ) )
112109, 111breqtrrd 4009 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( 2  x.  k
) )
113105lep1d 9642 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  k )  <_  ( ( 2  x.  k )  +  1 ) )
114103, 105, 107, 112, 113letrd 8927 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  k  <_  ( ( 2  x.  k )  +  1 ) )
115 nngt0 9729 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  0  <  k )
116115adantl 454 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  k )
11799nnred 9715 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR )
11899nngt0d 9743 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  0  <  ( ( 2  x.  k )  +  1 ) )
119 lerec 9592 . . . . . . . . . . . . 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 1188 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
k  <_  ( (
2  x.  k )  +  1 )  <->  ( 1  /  ( ( 2  x.  k )  +  1 ) )  <_ 
( 1  /  k
) ) )
121114, 120mpbid 203 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  <_  ( 1  / 
k ) )
122121, 98, 923brtr4d 4013 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) ) `  k
)  <_  ( (
n  e.  NN  |->  ( 1  /  n ) ) `  k ) )
12399nnrpd 10342 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 2  x.  k
)  +  1 )  e.  RR+ )
124123rpreccld 10353 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  /  ( ( 2  x.  k )  +  1 ) )  e.  RR+ )
125124rpge0d 10347 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( 1  /  (
( 2  x.  k
)  +  1 ) ) )
126125, 98breqtrrd 4009 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( n  e. 
NN0  |->  ( 1  / 
( ( 2  x.  n )  +  1 ) ) ) `  k ) )
12779, 81, 84, 87, 95, 101, 122, 126climsqz2 12066 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN0  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )  ~~>  0 )
128 neg1cn 9767 . . . . . . . . . . . . 13  |-  -u 1  e.  CC
129128a1i 12 . . . . . . . . . . . 12  |-  (  T. 
->  -u 1  e.  CC )
130 expcl 11073 . . . . . . . . . . . 12  |-  ( (
-u 1  e.  CC  /\  k  e.  NN0 )  ->  ( -u 1 ^ k )  e.  CC )
131129, 130sylan 459 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  ( -u 1 ^ k )  e.  CC )
13256nncnd 9716 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  e.  CC )
13356nnne0d 9744 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( 2  x.  k
)  +  1 )  =/=  0 )
134131, 132, 133divrecd 9493 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( -u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( -u
1 ^ k )  x.  ( 1  / 
( ( 2  x.  k )  +  1 ) ) ) )
135 oveq2 5786 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( -u 1 ^ n )  =  ( -u 1 ^ k ) )
136135, 73oveq12d 5796 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( -u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
137 eqid 2256 . . . . . . . . . . . 12  |-  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )  =  ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) )
138 ovex 5803 . . . . . . . . . . . 12  |-  ( (
-u 1 ^ k
)  /  ( ( 2  x.  k )  +  1 ) )  e.  _V
139136, 137, 138fvmpt 5522 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( (
-u 1 ^ n
)  /  ( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u
1 ^ k )  /  ( ( 2  x.  k )  +  1 ) ) )
140139adantl 454 . . . . . . . . . 10  |-  ( (  T.  /\  k  e. 
NN0 )  ->  (
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) `  k )  =  ( ( -u 1 ^ k )  /  (
( 2  x.  k
)  +  1 ) ) )
14177oveq2d 5794 . . . . . . . . . 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 2298 . . . . . . . . 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 12108 . . . . . . . 8  |-  (  T. 
->  seq  0 (  +  ,  ( n  e. 
NN0  |->  ( ( -u
1 ^ n )  /  ( ( 2  x.  n )  +  1 ) ) ) )  e.  dom  ~~>  )
144 climdm 11979 . . . . . . . 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 190 . . . . . . 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 5458 . . . . . . . 8  |-  (  ~~>  `  seq  0 (  +  , 
( n  e.  NN0  |->  ( ( -u 1 ^ n )  / 
( ( 2  x.  n )  +  1 ) ) ) ) )  e.  _V
147137, 20, 146leibpilem2 20185 . . . . . . 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 190 . . . . . 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 11000 . . . . . . 7  |-  seq  0
(  +  ,  ( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) ) ) )  e.  _V
150149, 146breldm 4857 . . . . . 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 17 . . . . 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 12172 . . . 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 2256 . . . . . . . 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 19766 . . . . . . 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 10316 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  n  e.  RR+ )
156155adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR+ )
157156rpreccld 10353 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR+ )
158157rpred 10343 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  RR )
159157rpge0d 10347 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  0  <_  ( 1  /  n
) )
160 nnge1 9726 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  1  <_  n )
161160adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  n )
162 nnre 9707 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  n  e.  RR )
163162adantl 454 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  RR )
164163recnd 8815 . . . . . . . . . . . . 13  |-  ( (  T.  /\  n  e.  NN )  ->  n  e.  CC )
165164mulid1d 8806 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  (
n  x.  1 )  =  n )
166161, 165breqtrrd 4009 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  1  <_  ( n  x.  1 ) )
1678a1i 12 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  RR )
168 nngt0 9729 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  0  <  n )
169168adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  n  e.  NN )  ->  0  <  n )
170 ledivmul 9583 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  1  e.  RR  /\  (
n  e.  RR  /\  0  <  n ) )  ->  ( ( 1  /  n )  <_ 
1  <->  1  <_  (
n  x.  1 ) ) )
171167, 167, 163, 169, 170syl112anc 1191 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 1  /  n
)  <_  1  <->  1  <_  ( n  x.  1 ) ) )
172166, 171mpbird 225 . . . . . . . . . 10  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  <_  1 )
173 0re 8792 . . . . . . . . . . 11  |-  0  e.  RR
174173, 8elicc2i 10668 . . . . . . . . . 10  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  <->  ( (
1  /  n )  e.  RR  /\  0  <_  ( 1  /  n
)  /\  ( 1  /  n )  <_ 
1 ) )
175158, 159, 172, 174syl3anbrc 1141 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  n )  e.  ( 0 [,] 1 ) )
176 iirev 18375 . . . . . . . . 9  |-  ( ( 1  /  n )  e.  ( 0 [,] 1 )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
177175, 176syl 17 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  ( 0 [,] 1 ) )
178 eqid 2256 . . . . . . . 8  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n
) ) )
179177, 178fmptd 5604 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) : NN --> ( 0 [,] 1
) )
18082a1i 12 . . . . . . . . 9  |-  (  T. 
->  1  e.  CC )
181 nnex 9706 . . . . . . . . . . 11  |-  NN  e.  _V
182181mptex 5666 . . . . . . . . . 10  |-  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) )  e.  _V
183182a1i 12 . . . . . . . . 9  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  e.  _V )
18495recnd 8815 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( 1  /  n
) ) `  k
)  e.  CC )
18588oveq2d 5794 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
1  -  ( 1  /  n ) )  =  ( 1  -  ( 1  /  k
) ) )
186 ovex 5803 . . . . . . . . . . . 12  |-  ( 1  -  ( 1  / 
k ) )  e. 
_V
187185, 178, 186fvmpt 5522 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( 1  / 
k ) ) )
18891oveq2d 5794 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `  k ) )  =  ( 1  -  ( 1  / 
k ) ) )
189187, 188eqtr4d 2291 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) ) `  k
)  =  ( 1  -  ( ( n  e.  NN  |->  ( 1  /  n ) ) `
 k ) ) )
190189adantl 454 . . . . . . . . 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 12063 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  ( 1  -  0 ) )
19282subid1i 9072 . . . . . . . 8  |-  ( 1  -  0 )  =  1
193191, 192syl6breq 4022 . . . . . . 7  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  ~~>  1 )
194 1elunit 10707 . . . . . . . 8  |-  1  e.  ( 0 [,] 1
)
195194a1i 12 . . . . . . 7  |-  (  T. 
->  1  e.  (
0 [,] 1 ) )
19679, 81, 154, 179, 193, 195climcncf 18352 . . . . . 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 2257 . . . . . . . 8  |-  (  T. 
->  ( n  e.  NN  |->  ( 1  -  (
1  /  n ) ) )  =  ( n  e.  NN  |->  ( 1  -  ( 1  /  n ) ) ) )
198 eqidd 2257 . . . . . . . 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 5785 . . . . . . . . . 10  |-  ( x  =  ( 1  -  ( 1  /  n
) )  ->  (
x ^ j )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
200199oveq2d 5794 . . . . . . . . 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 12128 . . . . . . . 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 5611 . . . . . . 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 12 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  ZZ )
20411adantll 697 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  (
( k  -  1 )  /  2 )  e.  NN0 )
2059, 204, 12sylancr 647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  RR )
206205recnd 8815 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k
) )  ->  ( -u 1 ^ ( ( k  -  1 )  /  2 ) )  e.  CC )
207206adantllr 702 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  e.  CC )
208 resubcl 9065 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
2098, 158, 208sylancr 647 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  RR )
210209ad2antrr 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( 1  -  ( 1  /  n
) )  e.  RR )
211 simplr 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN0 )
212210, 211reexpcld 11214 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  RR )
213212recnd 8815 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( 1  -  ( 1  /  n ) ) ^
k )  e.  CC )
214 nn0cn 9928 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  k  e.  CC )
215214ad2antlr 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  CC )
21614adantll 697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  e.  NN )
217216nnne0d 9744 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  k  =/=  0
)
218207, 213, 215, 217div12d 9526 . . . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k )  e.  CC )
220213, 219mulcomd 8810 . . . . . . . . . . . . . . . . . 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 2288 . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 3551 . . . . . . . . . . . . . . 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 8815 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  e.  CC )
225 expcl 11073 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  -  (
1  /  n ) )  e.  CC  /\  k  e.  NN0 )  -> 
( ( 1  -  ( 1  /  n
) ) ^ k
)  e.  CC )
226224, 225sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
( 1  -  (
1  /  n ) ) ^ k )  e.  CC )
227226mul02d 8964 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  (
0  x.  ( ( 1  -  ( 1  /  n ) ) ^ k ) )  =  0 )
228227ifeq1d 3539 . . . . . . . . . . . . . . 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 2291 . . . . . . . . . . . . . 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 5785 . . . . . . . . . . . . . . 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 5785 . . . . . . . . . . . . . . 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 3534 . . . . . . . . . . . . . 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 2306 . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
235 c0ex 8786 . . . . . . . . . . . . . . 15  |-  0  e.  _V
236 ovex 5803 . . . . . . . . . . . . . . 15  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) )  e.  _V
237235, 236ifex 3583 . . . . . . . . . . . . . 14  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^
k )  /  k
) ) )  e. 
_V
238 eqid 2256 . . . . . . . . . . . . . . 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 5528 . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . 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 5803 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  /  k )  e.  _V
242235, 241ifex 3583 . . . . . . . . . . . . . . 15  |-  if ( ( k  =  0  \/  2  ||  k
) ,  0 ,  ( ( -u 1 ^ ( ( k  -  1 )  / 
2 ) )  / 
k ) )  e. 
_V
24320fvmpt2 5528 . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . 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 5793 . . . . . . . . . . . . 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 2298 . . . . . . . . . . . 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 2599 . . . . . . . . . . 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 1629 . . . . . . . . . . . 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 4069 . . . . . . . . . . . . . 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 2392 . . . . . . . . . . . . . 14  |-  F/_ k
j
251249, 250nffv 5451 . . . . . . . . . . . . 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 4069 . . . . . . . . . . . . . . 15  |-  F/_ k
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  /  k ) ) )
253252, 250nffv 5451 . . . . . . . . . . . . . 14  |-  F/_ k
( ( k  e. 
NN0  |->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  /  k
) ) ) `  j )
254 nfcv 2392 . . . . . . . . . . . . . 14  |-  F/_ k  x.
255 nfcv 2392 . . . . . . . . . . . . . 14  |-  F/_ k
( ( 1  -  ( 1  /  n
) ) ^ j
)
256253, 254, 255nfov 5801 . . . . . . . . . . . . 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 2399 . . . . . . . . . . . 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 5444 . . . . . . . . . . . . 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 5444 . . . . . . . . . . . . . 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 5786 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( 1  -  (
1  /  n ) ) ^ k )  =  ( ( 1  -  ( 1  /  n ) ) ^
j ) )
261259, 260oveq12d 5796 . . . . . . . . . . . . 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 2270 . . . . . . . . . . . 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 2730 . . . . . . . . . . 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 190 . . . . . . . . . 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 2614 . . . . . . . . 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 12 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( k  =  0  \/  2  ||  k ) )  -> 
0  e.  CC )
267212, 216nndivred 9748 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  RR )
268267recnd 8815 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  n  e.  NN )  /\  k  e.  NN0 )  /\  ( -.  k  =  0  /\  -.  2  ||  k ) )  ->  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k )  e.  CC )
269207, 268mulcld 8809 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . 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 3552 . . . . . . . . . . . 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 5604 . . . . . . . . . . 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 5583 . . . . . . . . . . 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 459 . . . . . . . . . 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 2331 . . . . . . . . 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 9933 . . . . . . . . . . . 12  |-  0  e.  NN0
277276a1i 12 . . . . . . . . . . 11  |-  ( (  T.  /\  n  e.  NN )  ->  0  e.  NN0 )
278 0p1e1 9793 . . . . . . . . . . . . 13  |-  ( 0  +  1 )  =  1
279 seqeq1 11001 . . . . . . . . . . . . 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 10 . . . . . . . . . . . 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 12 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  1  e.  ZZ )
282 elnnuz 10217 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN  <->  j  e.  ( ZZ>= `  1 )
)
283 nnne0 9732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  k  =/=  0 )
284283neneqd 2435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN  ->  -.  k  =  0 )
285 biorf 396 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  k  =  0  -> 
( 2  ||  k  <->  ( k  =  0  \/  2  ||  k ) ) )
286284, 285syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  (
2  ||  k  <->  ( k  =  0  \/  2 
||  k ) ) )
287286bicomd 194 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  (
( k  =  0  \/  2  ||  k
)  <->  2  ||  k
) )
288287ifbid 3543 . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . 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 3583 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 2  ||  k ,  0 ,  ( (
-u 1 ^ (
( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  (
1  /  n ) ) ^ k )  /  k ) ) )  e.  _V
291 eqid 2256 . . . . . . . . . . . . . . . . . . . . . 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 5528 . . . . . . . . . . . . . . . . . . . . 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 655 . . . . . . . . . . . . . . . . . . . 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 2298 . . . . . . . . . . . . . . . . . . 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 2581 . . . . . . . . . . . . . . . . . 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 12 . . . . . . . . . . . . . . . . 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 1629 . . . . . . . . . . . . . . . . . 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 4069 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k
( k  e.  NN  |->  if ( 2  ||  k ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) ) )
299298, 250nffv 5451 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k
( ( k  e.  NN  |->  if ( 2 
||  k ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) ) ) `  j )
300251, 299nfeq 2399 . . . . . . . . . . . . . . . . . 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 5444 . . . . . . . . . . . . . . . . . . 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 2270 . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . 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 190 . . . . . . . . . . . . . . . 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 2614 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 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 11023 . . . . . . . . . . . . 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 11865 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  =  ( 1  -  (
1  /  n ) ) )
309 ltsubrp 10338 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  ( 1  /  n
)  e.  RR+ )  ->  ( 1  -  (
1  /  n ) )  <  1 )
3108, 157, 309sylancr 647 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  -  ( 1  /  n ) )  <  1 )
311308, 310eqbrtrd 4003 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  n  e.  NN )  ->  ( abs `  ( 1  -  ( 1  /  n
) ) )  <  1 )
312291atantayl2 20182 . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . 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 4003 . . . . . . . . . . . 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 4016 . . . . . . . . . . 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 12080 . . . . . . . . . 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 11011 . . . . . . . . . . . . . 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 10 . . . . . . . . . . . . 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 3531 . . . . . . . . . . . . . . . 16  |-  ( ( k  =  0  \/  2  ||  k )  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u 1 ^ ( ( k  - 
1 )  /  2
) )  x.  (
( ( 1  -  ( 1  /  n
) ) ^ k
)  /  k ) ) )  =  0 )
320319orcs 385 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  if ( ( k  =  0  \/  2  ||  k ) ,  0 ,  ( ( -u
1 ^ ( ( k  -  1 )  /  2 ) )  x.  ( ( ( 1  -  ( 1  /  n ) ) ^ k )  / 
k ) ) )  =  0 )
321320, 238, 235fvmpt 5522 . . . . . . . . . . . . . 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 10 . . . . . . . . . . . . 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 2276 . . . . . . . . . . . 12  |-  (  seq  0 (  +  , 
( k  e.  NN0  |->  if ( ( k  =  0  \/  2  ||  k )