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

Theorem stirlinglem5 27804
Description: If  T is between  0 and  1, then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem5.1  |-  D  =  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) ) )
stirlinglem5.2  |-  E  =  ( j  e.  NN  |->  ( ( T ^
j )  /  j
) )
stirlinglem5.3  |-  F  =  ( j  e.  NN  |->  ( ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  +  ( ( T ^
j )  /  j
) ) )
stirlinglem5.4  |-  H  =  ( j  e.  NN0  |->  ( 2  x.  (
( 1  /  (
( 2  x.  j
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  j )  +  1 ) ) ) ) )
stirlinglem5.5  |-  G  =  ( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) )
stirlinglem5.6  |-  ( ph  ->  T  e.  RR+ )
stirlinglem5.7  |-  ( ph  ->  ( abs `  T
)  <  1 )
Assertion
Ref Expression
stirlinglem5  |-  ( ph  ->  seq  0 (  +  ,  H )  ~~>  ( log `  ( ( 1  +  T )  /  (
1  -  T ) ) ) )
Distinct variable groups:    ph, j    T, j
Allowed substitution hints:    D( j)    E( j)    F( j)    G( j)    H( j)

Proof of Theorem stirlinglem5
Dummy variables  i 
k  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10522 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
2 1z 10312 . . . . . 6  |-  1  e.  ZZ
32a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
4 stirlinglem5.1 . . . . . . . . 9  |-  D  =  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) ) )
54a1i 11 . . . . . . . 8  |-  ( ph  ->  D  =  ( j  e.  NN  |->  ( (
-u 1 ^ (
j  -  1 ) )  x.  ( ( T ^ j )  /  j ) ) ) )
6 ax-1cn 9049 . . . . . . . . . . . . . 14  |-  1  e.  CC
76a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  1  e.  CC )
87negcld 9399 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  -u 1  e.  CC )
9 nnm1nn0 10262 . . . . . . . . . . . . 13  |-  ( j  e.  NN  ->  (
j  -  1 )  e.  NN0 )
109adantl 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  ( j  -  1 )  e. 
NN0 )
118, 10expcld 11524 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( -u
1 ^ ( j  -  1 ) )  e.  CC )
12 nncn 10009 . . . . . . . . . . . 12  |-  ( j  e.  NN  ->  j  e.  CC )
1312adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  j  e.  CC )
14 stirlinglem5.6 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  RR+ )
1514rpred 10649 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  e.  RR )
1615recnd 9115 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e.  CC )
1716adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  T  e.  CC )
18 nnnn0 10229 . . . . . . . . . . . . 13  |-  ( j  e.  NN  ->  j  e.  NN0 )
1918adantl 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  j  e. 
NN0 )
2017, 19expcld 11524 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( T ^ j )  e.  CC )
21 nnne0 10033 . . . . . . . . . . . 12  |-  ( j  e.  NN  ->  j  =/=  0 )
2221adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  j  =/=  0 )
2311, 13, 20, 22div32d 9814 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( -u 1 ^ ( j  -  1 ) )  /  j
)  x.  ( T ^ j ) )  =  ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) ) )
247, 17pncan2d 9414 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( 1  +  T )  -  1 )  =  T )
2524eqcomd 2442 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN )  ->  T  =  ( ( 1  +  T )  -  1 ) )
2625oveq1d 6097 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( T ^ j )  =  ( ( ( 1  +  T )  - 
1 ) ^ j
) )
2726oveq2d 6098 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( -u 1 ^ ( j  -  1 ) )  /  j
)  x.  ( T ^ j ) )  =  ( ( (
-u 1 ^ (
j  -  1 ) )  /  j )  x.  ( ( ( 1  +  T )  -  1 ) ^
j ) ) )
2823, 27eqtr3d 2471 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( (
-u 1 ^ (
j  -  1 ) )  x.  ( ( T ^ j )  /  j ) )  =  ( ( (
-u 1 ^ (
j  -  1 ) )  /  j )  x.  ( ( ( 1  +  T )  -  1 ) ^
j ) ) )
2928mpteq2dva 4296 . . . . . . . 8  |-  ( ph  ->  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) ) )  =  ( j  e.  NN  |->  ( ( ( -u
1 ^ ( j  -  1 ) )  /  j )  x.  ( ( ( 1  +  T )  - 
1 ) ^ j
) ) ) )
305, 29eqtrd 2469 . . . . . . 7  |-  ( ph  ->  D  =  ( j  e.  NN  |->  ( ( ( -u 1 ^ ( j  -  1 ) )  /  j
)  x.  ( ( ( 1  +  T
)  -  1 ) ^ j ) ) ) )
3130seqeq3d 11332 . . . . . 6  |-  ( ph  ->  seq  1 (  +  ,  D )  =  seq  1 (  +  ,  ( j  e.  NN  |->  ( ( (
-u 1 ^ (
j  -  1 ) )  /  j )  x.  ( ( ( 1  +  T )  -  1 ) ^
j ) ) ) ) )
326a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  CC )
3332, 16addcld 9108 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  T
)  e.  CC )
34 eqid 2437 . . . . . . . . . . 11  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3534cnmetdval 18806 . . . . . . . . . 10  |-  ( ( 1  e.  CC  /\  ( 1  +  T
)  e.  CC )  ->  ( 1 ( abs  o.  -  )
( 1  +  T
) )  =  ( abs `  ( 1  -  ( 1  +  T ) ) ) )
3632, 33, 35syl2anc 644 . . . . . . . . 9  |-  ( ph  ->  ( 1 ( abs 
o.  -  ) (
1  +  T ) )  =  ( abs `  ( 1  -  (
1  +  T ) ) ) )
37 1m1e0 10069 . . . . . . . . . . . . . 14  |-  ( 1  -  1 )  =  0
3837a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  -  1 )  =  0 )
3938oveq1d 6097 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  1 )  -  T
)  =  ( 0  -  T ) )
4032, 32, 16subsub4d 9443 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  -  1 )  -  T
)  =  ( 1  -  ( 1  +  T ) ) )
41 df-neg 9295 . . . . . . . . . . . . . 14  |-  -u T  =  ( 0  -  T )
4241eqcomi 2441 . . . . . . . . . . . . 13  |-  ( 0  -  T )  = 
-u T
4342a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  T
)  =  -u T
)
4439, 40, 433eqtr3d 2477 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  -  (
1  +  T ) )  =  -u T
)
4544fveq2d 5733 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  (
1  -  ( 1  +  T ) ) )  =  ( abs `  -u T ) )
4616absnegd 12252 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  -u T
)  =  ( abs `  T ) )
47 stirlinglem5.7 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  T
)  <  1 )
4846, 47eqbrtrd 4233 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  -u T
)  <  1 )
4945, 48eqbrtrd 4233 . . . . . . . . 9  |-  ( ph  ->  ( abs `  (
1  -  ( 1  +  T ) ) )  <  1 )
5036, 49eqbrtrd 4233 . . . . . . . 8  |-  ( ph  ->  ( 1 ( abs 
o.  -  ) (
1  +  T ) )  <  1 )
51 cnxmet 18808 . . . . . . . . . 10  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
5251a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
53 1re 9091 . . . . . . . . . . 11  |-  1  e.  RR
5453a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
5554rexrd 9135 . . . . . . . . 9  |-  ( ph  ->  1  e.  RR* )
56 elbl2 18421 . . . . . . . . 9  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  RR* )  /\  ( 1  e.  CC  /\  ( 1  +  T )  e.  CC ) )  -> 
( ( 1  +  T )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( 1 ( abs  o.  -  ) ( 1  +  T ) )  <  1 ) )
5752, 55, 32, 33, 56syl22anc 1186 . . . . . . . 8  |-  ( ph  ->  ( ( 1  +  T )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( 1 ( abs  o.  -  ) ( 1  +  T ) )  <  1 ) )
5850, 57mpbird 225 . . . . . . 7  |-  ( ph  ->  ( 1  +  T
)  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
59 eqid 2437 . . . . . . . 8  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
6059logtayl2 20554 . . . . . . 7  |-  ( ( 1  +  T )  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  seq  1
(  +  ,  ( j  e.  NN  |->  ( ( ( -u 1 ^ ( j  - 
1 ) )  / 
j )  x.  (
( ( 1  +  T )  -  1 ) ^ j ) ) ) )  ~~>  ( log `  ( 1  +  T
) ) )
6158, 60syl 16 . . . . . 6  |-  ( ph  ->  seq  1 (  +  ,  ( j  e.  NN  |->  ( ( (
-u 1 ^ (
j  -  1 ) )  /  j )  x.  ( ( ( 1  +  T )  -  1 ) ^
j ) ) ) )  ~~>  ( log `  (
1  +  T ) ) )
6231, 61eqbrtrd 4233 . . . . 5  |-  ( ph  ->  seq  1 (  +  ,  D )  ~~>  ( log `  ( 1  +  T
) ) )
63 seqex 11326 . . . . . 6  |-  seq  1
(  +  ,  F
)  e.  _V
6463a1i 11 . . . . 5  |-  ( ph  ->  seq  1 (  +  ,  F )  e. 
_V )
65 stirlinglem5.2 . . . . . . . 8  |-  E  =  ( j  e.  NN  |->  ( ( T ^
j )  /  j
) )
6665a1i 11 . . . . . . 7  |-  ( ph  ->  E  =  ( j  e.  NN  |->  ( ( T ^ j )  /  j ) ) )
6766seqeq3d 11332 . . . . . 6  |-  ( ph  ->  seq  1 (  +  ,  E )  =  seq  1 (  +  ,  ( j  e.  NN  |->  ( ( T ^ j )  / 
j ) ) ) )
68 logtayl 20552 . . . . . . 7  |-  ( ( T  e.  CC  /\  ( abs `  T )  <  1 )  ->  seq  1 (  +  , 
( j  e.  NN  |->  ( ( T ^
j )  /  j
) ) )  ~~>  -u ( log `  ( 1  -  T ) ) )
6916, 47, 68syl2anc 644 . . . . . 6  |-  ( ph  ->  seq  1 (  +  ,  ( j  e.  NN  |->  ( ( T ^ j )  / 
j ) ) )  ~~> 
-u ( log `  (
1  -  T ) ) )
7067, 69eqbrtrd 4233 . . . . 5  |-  ( ph  ->  seq  1 (  +  ,  E )  ~~>  -u ( log `  ( 1  -  T ) ) )
71 simpr 449 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
7271, 1syl6eleq 2527 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
734a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  D  =  ( j  e.  NN  |->  ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) ) ) )
74 oveq1 6089 . . . . . . . . . . 11  |-  ( j  =  n  ->  (
j  -  1 )  =  ( n  - 
1 ) )
7574oveq2d 6098 . . . . . . . . . 10  |-  ( j  =  n  ->  ( -u 1 ^ ( j  -  1 ) )  =  ( -u 1 ^ ( n  - 
1 ) ) )
76 oveq2 6090 . . . . . . . . . . 11  |-  ( j  =  n  ->  ( T ^ j )  =  ( T ^ n
) )
77 id 21 . . . . . . . . . . 11  |-  ( j  =  n  ->  j  =  n )
7876, 77oveq12d 6100 . . . . . . . . . 10  |-  ( j  =  n  ->  (
( T ^ j
)  /  j )  =  ( ( T ^ n )  /  n ) )
7975, 78oveq12d 6100 . . . . . . . . 9  |-  ( j  =  n  ->  (
( -u 1 ^ (
j  -  1 ) )  x.  ( ( T ^ j )  /  j ) )  =  ( ( -u
1 ^ ( n  -  1 ) )  x.  ( ( T ^ n )  /  n ) ) )
8079adantl 454 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  n  e.  (
1 ... k ) )  /\  j  =  n )  ->  ( ( -u 1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  =  ( ( -u 1 ^ ( n  - 
1 ) )  x.  ( ( T ^
n )  /  n
) ) )
81 elfznn 11081 . . . . . . . . 9  |-  ( n  e.  ( 1 ... k )  ->  n  e.  NN )
8281adantl 454 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  n  e.  NN )
836a1i 11 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  1  e.  CC )
8483negcld 9399 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  -u 1  e.  CC )
85 nnm1nn0 10262 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  (
n  -  1 )  e.  NN0 )
8684, 85expcld 11524 . . . . . . . . . 10  |-  ( n  e.  NN  ->  ( -u 1 ^ ( n  -  1 ) )  e.  CC )
8782, 86syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( -u 1 ^ ( n  -  1 ) )  e.  CC )
8816ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  T  e.  CC )
8982nnnn0d 10275 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  n  e.  NN0 )
9088, 89expcld 11524 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( T ^ n )  e.  CC )
9182nncnd 10017 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  n  e.  CC )
9282nnne0d 10045 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  n  =/=  0 )
9390, 91, 92divcld 9791 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  (
( T ^ n
)  /  n )  e.  CC )
9487, 93mulcld 9109 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  (
( -u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  e.  CC )
9573, 80, 82, 94fvmptd 5811 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( D `  n )  =  ( ( -u
1 ^ ( n  -  1 ) )  x.  ( ( T ^ n )  /  n ) ) )
9695, 94eqeltrd 2511 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( D `  n )  e.  CC )
97 addcl 9073 . . . . . . 7  |-  ( ( n  e.  CC  /\  i  e.  CC )  ->  ( n  +  i )  e.  CC )
9897adantl 454 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
n  e.  CC  /\  i  e.  CC )
)  ->  ( n  +  i )  e.  CC )
9972, 96, 98seqcl 11344 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  ,  D ) `  k
)  e.  CC )
10065a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  E  =  ( j  e.  NN  |->  ( ( T ^ j )  / 
j ) ) )
10178adantl 454 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  n  e.  (
1 ... k ) )  /\  j  =  n )  ->  ( ( T ^ j )  / 
j )  =  ( ( T ^ n
)  /  n ) )
102100, 101, 82, 93fvmptd 5811 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( E `  n )  =  ( ( T ^ n )  /  n ) )
103102, 93eqeltrd 2511 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( E `  n )  e.  CC )
10472, 103, 98seqcl 11344 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  ,  E ) `  k
)  e.  CC )
105 simpll 732 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ph )
106 stirlinglem5.3 . . . . . . . . . 10  |-  F  =  ( j  e.  NN  |->  ( ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  +  ( ( T ^
j )  /  j
) ) )
107106a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  F  =  ( j  e.  NN  |->  ( ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  +  ( ( T ^
j )  /  j
) ) ) )
10879, 78oveq12d 6100 . . . . . . . . . 10  |-  ( j  =  n  ->  (
( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) )  +  ( ( T ^ j
)  /  j ) )  =  ( ( ( -u 1 ^ ( n  -  1 ) )  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) ) )
109108adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  =  n )  ->  (
( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) )  +  ( ( T ^ j
)  /  j ) )  =  ( ( ( -u 1 ^ ( n  -  1 ) )  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) ) )
110 simpr 449 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
11186adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( -u
1 ^ ( n  -  1 ) )  e.  CC )
11216adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  T  e.  CC )
113110nnnn0d 10275 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  n  e. 
NN0 )
114112, 113expcld 11524 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( T ^ n )  e.  CC )
115110nncnd 10017 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  CC )
116110nnne0d 10045 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  n  =/=  0 )
117114, 115, 116divcld 9791 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( T ^ n )  /  n )  e.  CC )
118111, 117mulcld 9109 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( (
-u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  e.  CC )
119118, 117addcld 9108 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( -u 1 ^ ( n  -  1 ) )  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) )  e.  CC )
120107, 109, 110, 119fvmptd 5811 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  =  ( ( ( -u
1 ^ ( n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  +  ( ( T ^
n )  /  n
) ) )
1214a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  D  =  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) ) ) )
12279adantl 454 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  =  n )  ->  (
( -u 1 ^ (
j  -  1 ) )  x.  ( ( T ^ j )  /  j ) )  =  ( ( -u
1 ^ ( n  -  1 ) )  x.  ( ( T ^ n )  /  n ) ) )
123121, 122, 110, 118fvmptd 5811 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( D `
 n )  =  ( ( -u 1 ^ ( n  - 
1 ) )  x.  ( ( T ^
n )  /  n
) ) )
124123eqcomd 2442 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( (
-u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  =  ( D `  n ) )
12565a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  =  ( j  e.  NN  |->  ( ( T ^
j )  /  j
) ) )
12678adantl 454 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  =  n )  ->  (
( T ^ j
)  /  j )  =  ( ( T ^ n )  /  n ) )
127125, 126, 110, 117fvmptd 5811 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( E `
 n )  =  ( ( T ^
n )  /  n
) )
128127eqcomd 2442 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( T ^ n )  /  n )  =  ( E `  n
) )
129124, 128oveq12d 6100 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( -u 1 ^ ( n  -  1 ) )  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) )  =  ( ( D `
 n )  +  ( E `  n
) ) )
130120, 129eqtrd 2469 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  =  ( ( D `  n )  +  ( E `  n ) ) )
131105, 82, 130syl2anc 644 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  n  e.  ( 1 ... k
) )  ->  ( F `  n )  =  ( ( D `
 n )  +  ( E `  n
) ) )
13272, 96, 103, 131seradd 11366 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  ,  F ) `  k
)  =  ( (  seq  1 (  +  ,  D ) `  k )  +  (  seq  1 (  +  ,  E ) `  k ) ) )
1331, 3, 62, 64, 70, 99, 104, 132climadd 12426 . . . 4  |-  ( ph  ->  seq  1 (  +  ,  F )  ~~>  ( ( log `  ( 1  +  T ) )  +  -u ( log `  (
1  -  T ) ) ) )
134 1rp 10617 . . . . . . . . 9  |-  1  e.  RR+
135134a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  RR+ )
136135, 14rpaddcld 10664 . . . . . . 7  |-  ( ph  ->  ( 1  +  T
)  e.  RR+ )
137136rpne0d 10654 . . . . . 6  |-  ( ph  ->  ( 1  +  T
)  =/=  0 )
13833, 137logcld 20469 . . . . 5  |-  ( ph  ->  ( log `  (
1  +  T ) )  e.  CC )
13932, 16subcld 9412 . . . . . 6  |-  ( ph  ->  ( 1  -  T
)  e.  CC )
14015, 54absltd 12233 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  T
)  <  1  <->  ( -u 1  <  T  /\  T  <  1 ) ) )
14147, 140mpbid 203 . . . . . . . . 9  |-  ( ph  ->  ( -u 1  < 
T  /\  T  <  1 ) )
142141simprd 451 . . . . . . . 8  |-  ( ph  ->  T  <  1 )
14315, 142gtned 9209 . . . . . . 7  |-  ( ph  ->  1  =/=  T )
14432, 16, 143subne0d 9421 . . . . . 6  |-  ( ph  ->  ( 1  -  T
)  =/=  0 )
145139, 144logcld 20469 . . . . 5  |-  ( ph  ->  ( log `  (
1  -  T ) )  e.  CC )
146138, 145negsubd 9418 . . . 4  |-  ( ph  ->  ( ( log `  (
1  +  T ) )  +  -u ( log `  ( 1  -  T ) ) )  =  ( ( log `  ( 1  +  T
) )  -  ( log `  ( 1  -  T ) ) ) )
147133, 146breqtrd 4237 . . 3  |-  ( ph  ->  seq  1 (  +  ,  F )  ~~>  ( ( log `  ( 1  +  T ) )  -  ( log `  (
1  -  T ) ) ) )
148 nn0uz 10521 . . . 4  |-  NN0  =  ( ZZ>= `  0 )
149 0z 10294 . . . . 5  |-  0  e.  ZZ
150149a1i 11 . . . 4  |-  ( ph  ->  0  e.  ZZ )
151 stirlinglem5.5 . . . . . 6  |-  G  =  ( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) )
152 2nn0 10239 . . . . . . . . 9  |-  2  e.  NN0
153152a1i 11 . . . . . . . 8  |-  ( j  e.  NN0  ->  2  e. 
NN0 )
154 id 21 . . . . . . . 8  |-  ( j  e.  NN0  ->  j  e. 
NN0 )
155153, 154nn0mulcld 10280 . . . . . . 7  |-  ( j  e.  NN0  ->  ( 2  x.  j )  e. 
NN0 )
156 nn0p1nn 10260 . . . . . . 7  |-  ( ( 2  x.  j )  e.  NN0  ->  ( ( 2  x.  j )  +  1 )  e.  NN )
157155, 156syl 16 . . . . . 6  |-  ( j  e.  NN0  ->  ( ( 2  x.  j )  +  1 )  e.  NN )
158151, 157fmpti 5893 . . . . 5  |-  G : NN0
--> NN
159158a1i 11 . . . 4  |-  ( ph  ->  G : NN0 --> NN )
160 2re 10070 . . . . . . . . 9  |-  2  e.  RR
161160a1i 11 . . . . . . . 8  |-  ( k  e.  NN0  ->  2  e.  RR )
162 nn0re 10231 . . . . . . . 8  |-  ( k  e.  NN0  ->  k  e.  RR )
163161, 162remulcld 9117 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2  x.  k )  e.  RR )
16453a1i 11 . . . . . . . . 9  |-  ( k  e.  NN0  ->  1  e.  RR )
165162, 164readdcld 9116 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  RR )
166161, 165remulcld 9117 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2  x.  ( k  +  1 ) )  e.  RR )
167 2rp 10618 . . . . . . . . 9  |-  2  e.  RR+
168167a1i 11 . . . . . . . 8  |-  ( k  e.  NN0  ->  2  e.  RR+ )
169162ltp1d 9942 . . . . . . . 8  |-  ( k  e.  NN0  ->  k  < 
( k  +  1 ) )
170162, 165, 168, 169ltmul2dd 10701 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2  x.  k )  < 
( 2  x.  (
k  +  1 ) ) )
171163, 166, 164, 170ltadd1dd 9638 . . . . . 6  |-  ( k  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  < 
( ( 2  x.  ( k  +  1 ) )  +  1 ) )
172151a1i 11 . . . . . . 7  |-  ( k  e.  NN0  ->  G  =  ( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) ) )
173 simpr 449 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  j  =  k )  ->  j  =  k )
174173oveq2d 6098 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  j  =  k )  ->  ( 2  x.  j
)  =  ( 2  x.  k ) )
175174oveq1d 6097 . . . . . . 7  |-  ( ( k  e.  NN0  /\  j  =  k )  ->  ( ( 2  x.  j )  +  1 )  =  ( ( 2  x.  k )  +  1 ) )
176 id 21 . . . . . . 7  |-  ( k  e.  NN0  ->  k  e. 
NN0 )
177 2cn 10071 . . . . . . . . . 10  |-  2  e.  CC
178177a1i 11 . . . . . . . . 9  |-  ( k  e.  NN0  ->  2  e.  CC )
179 nn0cn 10232 . . . . . . . . 9  |-  ( k  e.  NN0  ->  k  e.  CC )
180178, 179mulcld 9109 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2  x.  k )  e.  CC )
1816a1i 11 . . . . . . . 8  |-  ( k  e.  NN0  ->  1  e.  CC )
182180, 181addcld 9108 . . . . . . 7  |-  ( k  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e.  CC )
183172, 175, 176, 182fvmptd 5811 . . . . . 6  |-  ( k  e.  NN0  ->  ( G `
 k )  =  ( ( 2  x.  k )  +  1 ) )
184 simpr 449 . . . . . . . . 9  |-  ( ( k  e.  NN0  /\  j  =  ( k  +  1 ) )  ->  j  =  ( k  +  1 ) )
185184oveq2d 6098 . . . . . . . 8  |-  ( ( k  e.  NN0  /\  j  =  ( k  +  1 ) )  ->  ( 2  x.  j )  =  ( 2  x.  ( k  +  1 ) ) )
186185oveq1d 6097 . . . . . . 7  |-  ( ( k  e.  NN0  /\  j  =  ( k  +  1 ) )  ->  ( ( 2  x.  j )  +  1 )  =  ( ( 2  x.  (
k  +  1 ) )  +  1 ) )
187 peano2nn0 10261 . . . . . . 7  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
188179, 181addcld 9108 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  CC )
189178, 188mulcld 9109 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2  x.  ( k  +  1 ) )  e.  CC )
190189, 181addcld 9108 . . . . . . 7  |-  ( k  e.  NN0  ->  ( ( 2  x.  ( k  +  1 ) )  +  1 )  e.  CC )
191172, 186, 187, 190fvmptd 5811 . . . . . 6  |-  ( k  e.  NN0  ->  ( G `
 ( k  +  1 ) )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
192171, 183, 1913brtr4d 4243 . . . . 5  |-  ( k  e.  NN0  ->  ( G `
 k )  < 
( G `  (
k  +  1 ) ) )
193192adantl 454 . . . 4  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  <  ( G `  ( k  +  1 ) ) )
194 eldifi 3470 . . . . . . 7  |-  ( n  e.  ( NN  \  ran  G )  ->  n  e.  NN )
195194adantl 454 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  n  e.  NN )
1966a1i 11 . . . . . . . . . . 11  |-  ( n  e.  ( NN  \  ran  G )  ->  1  e.  CC )
197196negcld 9399 . . . . . . . . . 10  |-  ( n  e.  ( NN  \  ran  G )  ->  -u 1  e.  CC )
198194, 85syl 16 . . . . . . . . . 10  |-  ( n  e.  ( NN  \  ran  G )  ->  (
n  -  1 )  e.  NN0 )
199197, 198expcld 11524 . . . . . . . . 9  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -u 1 ^ ( n  -  1 ) )  e.  CC )
200199adantl 454 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( -u 1 ^ ( n  -  1 ) )  e.  CC )
20116adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  T  e.  CC )
202195nnnn0d 10275 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  n  e.  NN0 )
203201, 202expcld 11524 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( T ^ n )  e.  CC )
204195nncnd 10017 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  n  e.  CC )
205195nnne0d 10045 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  n  =/=  0 )
206203, 204, 205divcld 9791 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( T ^ n
)  /  n )  e.  CC )
207200, 206mulcld 9109 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( -u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  e.  CC )
208207, 206addcld 9108 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( ( -u 1 ^ ( n  - 
1 ) )  x.  ( ( T ^
n )  /  n
) )  +  ( ( T ^ n
)  /  n ) )  e.  CC )
209108, 106fvmptg 5805 . . . . . 6  |-  ( ( n  e.  NN  /\  ( ( ( -u
1 ^ ( n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  +  ( ( T ^
n )  /  n
) )  e.  CC )  ->  ( F `  n )  =  ( ( ( -u 1 ^ ( n  - 
1 ) )  x.  ( ( T ^
n )  /  n
) )  +  ( ( T ^ n
)  /  n ) ) )
210195, 208, 209syl2anc 644 . . . . 5  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( F `  n )  =  ( ( (
-u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  +  ( ( T ^ n )  /  n ) ) )
211 eldifn 3471 . . . . . . . . . . . 12  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  n  e.  ran  G )
212 0nn0 10237 . . . . . . . . . . . . . . . 16  |-  0  e.  NN0
213 1nn0 10238 . . . . . . . . . . . . . . . . 17  |-  1  e.  NN0
214152, 213num0h 10393 . . . . . . . . . . . . . . . 16  |-  1  =  ( ( 2  x.  0 )  +  1 )
215 oveq2 6090 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  0  ->  (
2  x.  j )  =  ( 2  x.  0 ) )
216215oveq1d 6097 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  0  ->  (
( 2  x.  j
)  +  1 )  =  ( ( 2  x.  0 )  +  1 ) )
217216eqeq2d 2448 . . . . . . . . . . . . . . . . 17  |-  ( j  =  0  ->  (
1  =  ( ( 2  x.  j )  +  1 )  <->  1  =  ( ( 2  x.  0 )  +  1 ) ) )
218217rspcev 3053 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  NN0  /\  1  =  ( (
2  x.  0 )  +  1 ) )  ->  E. j  e.  NN0  1  =  ( (
2  x.  j )  +  1 ) )
219212, 214, 218mp2an 655 . . . . . . . . . . . . . . 15  |-  E. j  e.  NN0  1  =  ( ( 2  x.  j
)  +  1 )
220151elrnmpt 5118 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  CC  ->  (
1  e.  ran  G  <->  E. j  e.  NN0  1  =  ( ( 2  x.  j )  +  1 ) ) )
2216, 220ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 1  e.  ran  G  <->  E. j  e.  NN0  1  =  ( ( 2  x.  j
)  +  1 ) )
222219, 221mpbir 202 . . . . . . . . . . . . . 14  |-  1  e.  ran  G
223222a1i 11 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  1  e.  ran  G )
224 eleq1 2497 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
n  e.  ran  G  <->  1  e.  ran  G ) )
225223, 224mpbird 225 . . . . . . . . . . . 12  |-  ( n  =  1  ->  n  e.  ran  G )
226211, 225nsyl 116 . . . . . . . . . . 11  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  n  =  1 )
227 nn1m1nn 10021 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (
n  =  1  \/  ( n  -  1 )  e.  NN ) )
228194, 227syl 16 . . . . . . . . . . . 12  |-  ( n  e.  ( NN  \  ran  G )  ->  (
n  =  1  \/  ( n  -  1 )  e.  NN ) )
229228ord 368 . . . . . . . . . . 11  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -.  n  =  1  ->  ( n  -  1 )  e.  NN ) )
230226, 229mpd 15 . . . . . . . . . 10  |-  ( n  e.  ( NN  \  ran  G )  ->  (
n  -  1 )  e.  NN )
231 nfcv 2573 . . . . . . . . . . . . . . . . . 18  |-  F/_ j NN
232 nfmpt1 4299 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ j
( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) )
233151, 232nfcxfr 2570 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j G
234233nfrn 5113 . . . . . . . . . . . . . . . . . 18  |-  F/_ j ran  G
235231, 234nfdif 3469 . . . . . . . . . . . . . . . . 17  |-  F/_ j
( NN  \  ran  G )
236235nfcri 2567 . . . . . . . . . . . . . . . 16  |-  F/ j  n  e.  ( NN 
\  ran  G )
237151elrnmpt 5118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ( NN  \  ran  G )  ->  (
n  e.  ran  G  <->  E. j  e.  NN0  n  =  ( ( 2  x.  j )  +  1 ) ) )
238211, 237mtbid 293 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  E. j  e.  NN0  n  =  ( ( 2  x.  j )  +  1 ) )
239 ralnex 2716 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. j  e.  NN0  -.  n  =  ( ( 2  x.  j )  +  1 )  <->  -.  E. j  e.  NN0  n  =  ( ( 2  x.  j
)  +  1 ) )
240238, 239sylibr 205 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( NN  \  ran  G )  ->  A. j  e.  NN0  -.  n  =  ( ( 2  x.  j )  +  1 ) )
241240r19.21bi 2805 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  ( NN 
\  ran  G )  /\  j  e.  NN0 )  ->  -.  n  =  ( ( 2  x.  j )  +  1 ) )
242241neneqad 2675 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  ( NN 
\  ran  G )  /\  j  e.  NN0 )  ->  n  =/=  (
( 2  x.  j
)  +  1 ) )
243242necomd 2688 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  ( NN 
\  ran  G )  /\  j  e.  NN0 )  ->  ( ( 2  x.  j )  +  1 )  =/=  n
)
244243adantlr 697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  ( NN  \  ran  G
)  /\  j  e.  ZZ )  /\  j  e.  NN0 )  ->  (
( 2  x.  j
)  +  1 )  =/=  n )
245 simplr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  ( NN  \  ran  G
)  /\  j  e.  ZZ )  /\  -.  j  e.  NN0 )  ->  j  e.  ZZ )
246 simpr 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  ( NN  \  ran  G
)  /\  j  e.  ZZ )  /\  -.  j  e.  NN0 )  ->  -.  j  e.  NN0 )
247194ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  ( NN  \  ran  G
)  /\  j  e.  ZZ )  /\  -.  j  e.  NN0 )  ->  n  e.  NN )
248160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  2  e.  RR )
249 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  j  e.  ZZ )
250249zred 10376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  j  e.  RR )
251248, 250remulcld 9117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( 2  x.  j )  e.  RR )
252 0re 9092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  RR
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  0  e.  RR )
25453a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  1  e.  RR )
255177a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  2  e.  CC )
256250recnd 9115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  j  e.  CC )
257255, 256mulcomd 9110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( 2  x.  j )  =  ( j  x.  2 ) )
258 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  -.  j  e.  NN0 )
259 elnn0z 10295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  e.  NN0  <->  ( j  e.  ZZ  /\  0  <_ 
j ) )
260258, 259sylnib 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  -.  ( j  e.  ZZ  /\  0  <_ 
j ) )
261 nan 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  ->  -.  ( j  e.  ZZ  /\  0  <_ 
j ) )  <->  ( (
( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  /\  j  e.  ZZ )  ->  -.  0  <_  j ) )
262260, 261mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  /\  j  e.  ZZ )  ->  -.  0  <_  j )
263262anabss1 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  -.  0  <_  j )
264250, 253ltnled 9221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( j  <  0  <->  -.  0  <_  j ) )
265263, 264mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  j  <  0
)
266167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  2  e.  RR+ )
267266rpregt0d 10655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( 2  e.  RR  /\  0  <  2 ) )
268 mulltgt0 27670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( j  e.  RR  /\  j  <  0 )  /\  ( 2  e.  RR  /\  0  <  2 ) )  -> 
( j  x.  2 )  <  0 )
269250, 265, 267, 268syl21anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( j  x.  2 )  <  0
)
270257, 269eqbrtrd 4233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( 2  x.  j )  <  0
)
271251, 253, 254, 270ltadd1dd 9638 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( ( 2  x.  j )  +  1 )  <  (
0  +  1 ) )
2726a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  1  e.  CC )
273272addid2d 9268 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( 0  +  1 )  =  1 )
274271, 273breqtrd 4237 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( ( 2  x.  j )  +  1 )  <  1
)
275251, 254readdcld 9116 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( ( 2  x.  j )  +  1 )  e.  RR )
276275, 254ltnled 9221 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  ( ( ( 2  x.  j )  +  1 )  <  1  <->  -.  1  <_  ( ( 2  x.  j
)  +  1 ) ) )
277274, 276mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  -.  1  <_  ( ( 2  x.  j
)  +  1 ) )
278 nnge1 10027 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2  x.  j
)  +  1 )  e.  NN  ->  1  <_  ( ( 2  x.  j )  +  1 ) )
279277, 278nsyl 116 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  ->  -.  ( (
2  x.  j )  +  1 )  e.  NN )
280279adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  /\  n  e.  NN )  ->  -.  ( (
2  x.  j )  +  1 )  e.  NN )
281 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  ( ( 2  x.  j )  +  1 )  =  n )  ->  ( ( 2  x.  j )  +  1 )  =  n )
282 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  ( ( 2  x.  j )  +  1 )  =  n )  ->  n  e.  NN )
283281, 282eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  ( ( 2  x.  j )  +  1 )  =  n )  ->  ( ( 2  x.  j )  +  1 )  e.  NN )
284283adantll 696 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( j  e.  ZZ  /\  -.  j  e.  NN0 )  /\  n  e.  NN )  /\  (
( 2  x.  j
)  +  1 )  =  n )  -> 
( ( 2  x.  j )  +  1 )  e.  NN )
285280, 284mtand 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  /\  n  e.  NN )  ->  -.  ( (
2  x.  j )  +  1 )  =  n )
286285neneqad 2675 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  e.  ZZ  /\ 
-.  j  e.  NN0 )  /\  n  e.  NN )  ->  ( ( 2  x.  j )  +  1 )  =/=  n
)
287245, 246, 247, 286syl21anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  ( NN  \  ran  G
)  /\  j  e.  ZZ )  /\  -.  j  e.  NN0 )  ->  (
( 2  x.  j
)  +  1 )  =/=  n )
288244, 287pm2.61dan 768 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  ( NN 
\  ran  G )  /\  j  e.  ZZ )  ->  ( ( 2  x.  j )  +  1 )  =/=  n
)
289288neneqd 2618 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( NN 
\  ran  G )  /\  j  e.  ZZ )  ->  -.  ( (
2  x.  j )  +  1 )  =  n )
290289ex 425 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( NN  \  ran  G )  ->  (
j  e.  ZZ  ->  -.  ( ( 2  x.  j )  +  1 )  =  n ) )
291236, 290ralrimi 2788 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( NN  \  ran  G )  ->  A. j  e.  ZZ  -.  ( ( 2  x.  j )  +  1 )  =  n )
292 ralnex 2716 . . . . . . . . . . . . . . 15  |-  ( A. j  e.  ZZ  -.  ( ( 2  x.  j )  +  1 )  =  n  <->  -.  E. j  e.  ZZ  ( ( 2  x.  j )  +  1 )  =  n )
293291, 292sylib 190 . . . . . . . . . . . . . 14  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  E. j  e.  ZZ  (
( 2  x.  j
)  +  1 )  =  n )
294194nnzd 10375 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( NN  \  ran  G )  ->  n  e.  ZZ )
295 odd2np1 12909 . . . . . . . . . . . . . . 15  |-  ( n  e.  ZZ  ->  ( -.  2  ||  n  <->  E. j  e.  ZZ  ( ( 2  x.  j )  +  1 )  =  n ) )
296294, 295syl 16 . . . . . . . . . . . . . 14  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -.  2  ||  n  <->  E. j  e.  ZZ  ( ( 2  x.  j )  +  1 )  =  n ) )
297293, 296mtbird 294 . . . . . . . . . . . . 13  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  -.  2  ||  n )
298297notnotrd 108 . . . . . . . . . . . 12  |-  ( n  e.  ( NN  \  ran  G )  ->  2  ||  n )
299194nncnd 10017 . . . . . . . . . . . . 13  |-  ( n  e.  ( NN  \  ran  G )  ->  n  e.  CC )
300299, 196npcand 9416 . . . . . . . . . . . 12  |-  ( n  e.  ( NN  \  ran  G )  ->  (
( n  -  1 )  +  1 )  =  n )
301298, 300breqtrrd 4239 . . . . . . . . . . 11  |-  ( n  e.  ( NN  \  ran  G )  ->  2  ||  ( ( n  - 
1 )  +  1 ) )
302198nn0zd 10374 . . . . . . . . . . . 12  |-  ( n  e.  ( NN  \  ran  G )  ->  (
n  -  1 )  e.  ZZ )
303 oddp1even 12911 . . . . . . . . . . . 12  |-  ( ( n  -  1 )  e.  ZZ  ->  ( -.  2  ||  ( n  -  1 )  <->  2  ||  ( ( n  - 
1 )  +  1 ) ) )
304302, 303syl 16 . . . . . . . . . . 11  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -.  2  ||  ( n  -  1 )  <->  2  ||  ( ( n  - 
1 )  +  1 ) ) )
305301, 304mpbird 225 . . . . . . . . . 10  |-  ( n  e.  ( NN  \  ran  G )  ->  -.  2  ||  ( n  - 
1 ) )
306 oexpneg 12912 . . . . . . . . . 10  |-  ( ( 1  e.  CC  /\  ( n  -  1
)  e.  NN  /\  -.  2  ||  ( n  -  1 ) )  ->  ( -u 1 ^ ( n  - 
1 ) )  = 
-u ( 1 ^ ( n  -  1 ) ) )
307196, 230, 305, 306syl3anc 1185 . . . . . . . . 9  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -u 1 ^ ( n  -  1 ) )  =  -u ( 1 ^ ( n  -  1 ) ) )
308 1exp 11410 . . . . . . . . . . 11  |-  ( ( n  -  1 )  e.  ZZ  ->  (
1 ^ ( n  -  1 ) )  =  1 )
309302, 308syl 16 . . . . . . . . . 10  |-  ( n  e.  ( NN  \  ran  G )  ->  (
1 ^ ( n  -  1 ) )  =  1 )
310309negeqd 9301 . . . . . . . . 9  |-  ( n  e.  ( NN  \  ran  G )  ->  -u (
1 ^ ( n  -  1 ) )  =  -u 1 )
311307, 310eqtrd 2469 . . . . . . . 8  |-  ( n  e.  ( NN  \  ran  G )  ->  ( -u 1 ^ ( n  -  1 ) )  =  -u 1 )
312311adantl 454 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( -u 1 ^ ( n  -  1 ) )  =  -u 1 )
313312oveq1d 6097 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( -u 1 ^ (
n  -  1 ) )  x.  ( ( T ^ n )  /  n ) )  =  ( -u 1  x.  ( ( T ^
n )  /  n
) ) )
314313oveq1d 6097 . . . . 5  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( ( -u 1 ^ ( n  - 
1 ) )  x.  ( ( T ^
n )  /  n
) )  +  ( ( T ^ n
)  /  n ) )  =  ( (
-u 1  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) ) )
315206mulm1d 9486 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( -u 1  x.  ( ( T ^ n )  /  n ) )  =  -u ( ( T ^ n )  /  n ) )
316315oveq1d 6097 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( -u 1  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) )  =  ( -u (
( T ^ n
)  /  n )  +  ( ( T ^ n )  /  n ) ) )
317206negcld 9399 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  -u (
( T ^ n
)  /  n )  e.  CC )
318317, 206addcomd 9269 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( -u ( ( T ^
n )  /  n
)  +  ( ( T ^ n )  /  n ) )  =  ( ( ( T ^ n )  /  n )  + 
-u ( ( T ^ n )  /  n ) ) )
319206negidd 9402 . . . . . 6  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( ( T ^
n )  /  n
)  +  -u (
( T ^ n
)  /  n ) )  =  0 )
320316, 318, 3193eqtrd 2473 . . . . 5  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  (
( -u 1  x.  (
( T ^ n
)  /  n ) )  +  ( ( T ^ n )  /  n ) )  =  0 )
321210, 314, 3203eqtrd 2473 . . . 4  |-  ( (
ph  /\  n  e.  ( NN  \  ran  G
) )  ->  ( F `  n )  =  0 )
322120, 119eqeltrd 2511 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e.  CC )
323106a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  F  =  ( j  e.  NN  |->  ( ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  +  ( ( T ^
j )  /  j
) ) ) )
324 simpr 449 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
j  =  ( ( 2  x.  k )  +  1 ) )
325324oveq1d 6097 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( j  -  1 )  =  ( ( ( 2  x.  k
)  +  1 )  -  1 ) )
326325oveq2d 6098 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( -u 1 ^ (
j  -  1 ) )  =  ( -u
1 ^ ( ( ( 2  x.  k
)  +  1 )  -  1 ) ) )
327324oveq2d 6098 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( T ^ j
)  =  ( T ^ ( ( 2  x.  k )  +  1 ) ) )
328327, 324oveq12d 6100 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( ( T ^
j )  /  j
)  =  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) )
329326, 328oveq12d 6100 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( ( -u 1 ^ ( j  - 
1 ) )  x.  ( ( T ^
j )  /  j
) )  =  ( ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  -  1 ) )  x.  (
( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
330329, 328oveq12d 6100 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  ( ( 2  x.  k )  +  1 ) )  -> 
( ( ( -u
1 ^ ( j  -  1 ) )  x.  ( ( T ^ j )  / 
j ) )  +  ( ( T ^
j )  /  j
) )  =  ( ( ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  - 
1 ) )  x.  ( ( T ^
( ( 2  x.  k )  +  1 ) )  /  (
( 2  x.  k
)  +  1 ) ) )  +  ( ( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
331152a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  2  e.  NN0 )
332 simpr 449 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  NN0 )
333331, 332nn0mulcld 10280 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  k )  e. 
NN0 )
334 nn0p1nn 10260 . . . . . . . 8  |-  ( ( 2  x.  k )  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
335333, 334syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
2  x.  k )  +  1 )  e.  NN )
336181negcld 9399 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  -u 1  e.  CC )
337180, 181pncand 9413 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  k
)  +  1 )  -  1 )  =  ( 2  x.  k
) )
338152a1i 11 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  2  e. 
NN0 )
339338, 176nn0mulcld 10280 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( 2  x.  k )  e. 
NN0 )
340337, 339eqeltrd 2511 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  k
)  +  1 )  -  1 )  e. 
NN0 )
341336, 340expcld 11524 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( -u
1 ^ ( ( ( 2  x.  k
)  +  1 )  -  1 ) )  e.  CC )
342341adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  - 
1 ) )  e.  CC )
34316adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  T  e.  CC )
344213a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  1  e.  NN0 )
345333, 344nn0addcld 10279 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
2  x.  k )  +  1 )  e. 
NN0 )
346343, 345expcld 11524 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( T ^ ( ( 2  x.  k )  +  1 ) )  e.  CC )
347177a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  2  e.  CC )
348179adantl 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  CC )
349347, 348mulcld 9109 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  k )  e.  CC )
3506a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  1  e.  CC )
351349, 350addcld 9108 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
2  x.  k )  +  1 )  e.  CC )
352252a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  e.  RR )
353160a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  2  e.  RR )
354162adantl 454 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  RR )
355353, 354remulcld 9117 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  k )  e.  RR )
35653a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  1  e.  RR )
357152nn0ge0i 10250 . . . . . . . . . . . . . 14  |-  0  <_  2
358357a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  <_  2 )
359332nn0ge0d 10278 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  <_  k )
360353, 354, 358, 359mulge0d 9604 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  <_  ( 2  x.  k ) )
361 0lt1 9551 . . . . . . . . . . . . 13  |-  0  <  1
362361a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  <  1 )
363355, 356, 360, 362addgegt0d 9601 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  0  <  ( ( 2  x.  k
)  +  1 ) )
364352, 363gtned 9209 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
2  x.  k )  +  1 )  =/=  0 )
365346, 351, 364divcld 9791 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) )  e.  CC )
366342, 365mulcld 9109 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( -u 1 ^ ( ( ( 2  x.  k
)  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  e.  CC )
367366, 365addcld 9108 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( -u 1 ^ (
( ( 2  x.  k )  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) )  +  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  e.  CC )
368323, 330, 335, 367fvmptd 5811 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( ( 2  x.  k )  +  1 ) )  =  ( ( ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  - 
1 ) )  x.  ( ( T ^
( ( 2  x.  k )  +  1 ) )  /  (
( 2  x.  k
)  +  1 ) ) )  +  ( ( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
369337adantl 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( 2  x.  k
)  +  1 )  -  1 )  =  ( 2  x.  k
) )
370369oveq2d 6098 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  - 
1 ) )  =  ( -u 1 ^ ( 2  x.  k
) ) )
371 m1expeven 27702 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( -u
1 ^ ( 2  x.  k ) )  =  1 )
372371adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( -u 1 ^ ( 2  x.  k ) )  =  1 )
373370, 372eqtrd 2469 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( -u 1 ^ ( ( ( 2  x.  k )  +  1 )  - 
1 ) )  =  1 )
374373oveq1d 6097 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( -u 1 ^ ( ( ( 2  x.  k
)  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( 1  x.  (
( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
375365mulid2d 9107 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( ( T ^
( ( 2  x.  k )  +  1 ) )  /  (
( 2  x.  k
)  +  1 ) ) )
376374, 375eqtrd 2469 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( -u 1 ^ ( ( ( 2  x.  k
)  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( ( T ^
( ( 2  x.  k )  +  1 ) )  /  (
( 2  x.  k
)  +  1 ) ) )
377376oveq1d 6097 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( -u 1 ^ (
( ( 2  x.  k )  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) )  +  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) )  +  ( ( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
3783652timesd 10211 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) )  +  ( ( T ^ (
( 2  x.  k
)  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) ) )
379346, 351, 364divrec2d 9795 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) )  =  ( ( 1  /  (
( 2  x.  k
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  k )  +  1 ) ) ) )
380379oveq2d 6098 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( 2  x.  (
( 1  /  (
( 2  x.  k
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  k )  +  1 ) ) ) ) )
381377, 378, 3803eqtr2d 2475 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( -u 1 ^ (
( ( 2  x.  k )  +  1 )  -  1 ) )  x.  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  /  ( ( 2  x.  k )  +  1 ) ) )  +  ( ( T ^ ( ( 2  x.  k )  +  1 ) )  / 
( ( 2  x.  k )  +  1 ) ) )  =  ( 2  x.  (
( 1  /  (
( 2  x.  k
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  k )  +  1 ) ) ) ) )
382368, 381eqtr2d 2470 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  ( ( 1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^ (
( 2  x.  k
)  +  1 ) ) ) )  =  ( F `  (
( 2  x.  k
)  +  1 ) ) )
383 stirlinglem5.4 . . . . . . 7  |-  H  =  ( j  e.  NN0  |->  ( 2  x.  (
( 1  /  (
( 2  x.  j
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  j )  +  1 ) ) ) ) )
384383a1i 11 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  H  =  ( j  e.  NN0  |->  ( 2  x.  (
( 1  /  (
( 2  x.  j
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  j )  +  1 ) ) ) ) ) )
385 simpr 449 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
j  =  k )
386385oveq2d 6098 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( 2  x.  j
)  =  ( 2  x.  k ) )
387386oveq1d 6097 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( ( 2  x.  j )  +  1 )  =  ( ( 2  x.  k )  +  1 ) )
388387oveq2d 6098 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( 1  /  (
( 2  x.  j
)  +  1 ) )  =  ( 1  /  ( ( 2  x.  k )  +  1 ) ) )
389387oveq2d 6098 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( T ^ (
( 2  x.  j
)  +  1 ) )  =  ( T ^ ( ( 2  x.  k )  +  1 ) ) )
390388, 389oveq12d 6100 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( ( 1  / 
( ( 2  x.  j )  +  1 ) )  x.  ( T ^ ( ( 2  x.  j )  +  1 ) ) )  =  ( ( 1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^ (
( 2  x.  k
)  +  1 ) ) ) )
391390oveq2d 6098 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( 2  x.  (
( 1  /  (
( 2  x.  j
)  +  1 ) )  x.  ( T ^ ( ( 2  x.  j )  +  1 ) ) ) )  =  ( 2  x.  ( ( 1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^ (
( 2  x.  k
)  +  1 ) ) ) ) )
392351, 364reccld 9784 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( ( 2  x.  k )  +  1 ) )  e.  CC )
393392, 346mulcld 9109 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^
( ( 2  x.  k )  +  1 ) ) )  e.  CC )
394347, 393mulcld 9109 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2  x.  ( ( 1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^ (
( 2  x.  k
)  +  1 ) ) ) )  e.  CC )
395384, 391, 332, 394fvmptd 5811 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( H `  k )  =  ( 2  x.  ( ( 1  /  ( ( 2  x.  k )  +  1 ) )  x.  ( T ^
( ( 2  x.  k )  +  1 ) ) ) ) )
396213a1i 11 . . . . . . . . 9  |-  ( k  e.  NN0  ->  1  e. 
NN0 )
397339, 396nn0addcld 10279 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 2  x.  k )  +  1 )  e. 
NN0 )
398172, 175, 176, 397fvmptd 5811 . . . . . . 7  |-  ( k  e.  NN0  ->  ( G `
 k )  =  ( ( 2  x.  k )  +  1 ) )
399398adantl 454 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  =  ( ( 2  x.  k
)  +  1 ) )
400399fveq2d 5733 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( G `  k
) )  =  ( F `  ( ( 2  x.  k )  +  1 ) ) )
401382, 395, 4003eqtr4d 2479 . . . 4  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( H `  k )  =  ( F `  ( G `
 k ) ) )
402148, 1, 150, 3, 159, 193, 321, 322, 401isercoll2 12463 . . 3  |-  ( ph  ->  (  seq  0 (  +  ,  H )  ~~>  ( ( log `  (
1  +  T ) )  -  ( log `  ( 1  -  T
) ) )  <->  seq  1
(  +  ,  F
)  ~~>  ( ( log `  ( 1  +  T
) )  -  ( log `  ( 1  -  T ) ) ) ) )
403147, 402mpbird 225 . 2  |-  ( ph  ->  seq  0 (  +  ,  H )  ~~>  ( ( log `  ( 1  +  T ) )  -  ( log `  (
1  -  T ) ) ) )
40454, 15resubcld 9466 . . . 4  |-  ( ph  ->  ( 1  -  T
)  e.  RR )
40516subidd 9400 . . . . . 6  |-  ( ph  ->  ( T  -  T
)  =  0 )
406405eqcomd 2442 . . . . 5  |-  ( ph  ->  0  =  ( T  -  T ) )
40715, 54, 15, 142ltsub1dd 9639 . . . . 5  |-  ( ph  ->  ( T  -  T
)  <  ( 1  -  T ) )
408406, 407eqbrtrd 4233 . . . 4  |-  ( ph  ->  0  <  ( 1  -  T ) )
409404, 408elrpd 10647 . . 3  |-  ( ph  ->  ( 1  -  T
)  e.  RR+ )
410136, 409relogdivd 20522 . 2  |-  ( ph  ->  ( log `  (
( 1  +  T
)  /  ( 1  -  T ) ) )  =  ( ( log `  ( 1  +  T ) )  -  ( log `  (
1  -  T ) ) ) )
411403, 410breqtrrd 4239 1  |-  ( ph  ->  seq  0 (  +  ,  H )  ~~>  ( log `  ( ( 1  +  T )  /  (
1  -  T ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2600   A.wral 2706   E.wrex 2707   _Vcvv 2957    \ cdif 3318   class class class wbr 4213    e. cmpt 4267   ran crn 4880    o. ccom 4883   -->wf 5451   ` cfv 5455  (class class class)co 6082   CCcc 8989   RRcr 8990   0cc0 8991   1c1 8992    + caddc 8994    x. cmul 8996   RR*cxr 9120    < clt 9121    <_ cle 9122    - cmin 9292   -ucneg 9293    / cdiv 9678   NNcn 10001   2c2 10050   NN0cn0 10222   ZZcz 10283   ZZ>=cuz 10489   RR+crp 10613   ...cfz 11044    seq cseq 11324   ^cexp 11383   abscabs 12040    ~~> cli 12279    || cdivides 12853   * Metcxmt 16687   ballcbl 16689   logclog 20453
This theorem is referenced by:  stirlinglem6  27805
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069  ax-addf 9070  ax-mulf 9071
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-iin 4097  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6306  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-2o 6726  df-oadd 6729  df-er 6906  df-map 7021  df-pm 7022  df-ixp 7065  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-fi 7417  df-sup 7447  df-oi 7480  df-card 7827  df-cda 8049  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-4 10061  df-5 10062  df-6 10063  df-7 10064  df-8 10065  df-9 10066  df-10 10067  df-n0 10223  df-z 10284  df-dec 10384  df-uz 10490  df-q 10576  df-rp 10614  df-xneg 10711  df-xadd 10712  df-xmul 10713  df-ioo 10921  df-ioc 10922  df-ico 10923  df-icc 10924  df-fz 11045  df-fzo 11137  df-fl 11203  df-mod 11252  df-seq 11325  df-exp 11384  df-fac 11568  df-bc 11595  df-hash 11620  df-shft 11883  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-limsup 12266  df-clim 12283  df-rlim 12284  df-sum 12481  df-ef 12671  df-sin 12673  df-cos 12674  df-tan 12675  df-pi 12676  df-dvds 12854  df-struct 13472  df-ndx 13473  df-slot 13474  df-base 13475  df-sets 13476  df-ress 13477  df-plusg 13543  df-mulr 13544  df-starv 13545  df-sca 13546  df-vsca 13547  df-tset 13549  df-ple 13550  df-ds 13552  df-unif 13553  df-hom 13554  df-cco 13555  df-rest 13651  df-topn 13652  df-topgen 13668  df-pt 13669  df-prds 13672  df-xrs 13727  df-0g 13728  df-gsum 13729  df-qtop 13734  df-imas 13735  df-xps 13737  df-mre 13812  df-mrc 13813  df-acs 13815  df-mnd 14691  df-submnd 14740  df-mulg 14816  df-cntz 15117  df-cmn 15415  df-psmet 16695  df-xmet 16696  df-met 16697  df-bl 16698  df-mopn 16699  df-fbas 16700  df-fg 16701  df-cnfld 16705  df-top 16964  df-bases 16966  df-topon 16967  df-topsp 16968  df-cld 17084  df-ntr 17085  df-cls 17086  df-nei 17163  df-lp 17201  df-perf 17202  df-cn 17292  df-cnp 17293  df-haus 17380  df-cmp 17451  df-tx 17595  df-hmeo 17788  df-fil 17879  df-fm 17971  df-flim 17972  df-flf 17973  df-xms 18351  df-ms 18352  df-tms 18353  df-cncf 18909  df-limc 19754  df-dv 19755  df-ulm 20294  df-log 20455
  Copyright terms: Public domain W3C validator