This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stirlinglem5

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)

Ref Expression
Hypotheses 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 stirlinglem5 
|- ( ph -> seq 0 ( + , H ) ~~> ( log ` ( ( 1 + T ) / ( 1 - T ) ) ) )

Proof

Step Hyp Ref Expression
1 stirlinglem5.1 
 |-  D = ( j e. NN |-> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) )
2 stirlinglem5.2 
 |-  E = ( j e. NN |-> ( ( T ^ j ) / j ) )
3 stirlinglem5.3 
 |-  F = ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) + ( ( T ^ j ) / j ) ) )
4 stirlinglem5.4 
 |-  H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( T ^ ( ( 2 x. j ) + 1 ) ) ) ) )
5 stirlinglem5.5 
 |-  G = ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) )
6 stirlinglem5.6 
 |-  ( ph -> T e. RR+ )
7 stirlinglem5.7 
 |-  ( ph -> ( abs ` T ) < 1 )
8 nnuz 
 |-  NN = ( ZZ>= ` 1 )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 1 a1i 
 |-  ( ph -> D = ( j e. NN |-> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) ) )
11 1cnd 
 |-  ( ( ph /\ j e. NN ) -> 1 e. CC )
12 11 negcld 
 |-  ( ( ph /\ j e. NN ) -> -u 1 e. CC )
13 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
14 13 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( j - 1 ) e. NN0 )
15 12 14 expcld 
 |-  ( ( ph /\ j e. NN ) -> ( -u 1 ^ ( j - 1 ) ) e. CC )
16 nncn 
 |-  ( j e. NN -> j e. CC )
17 16 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. CC )
18 6 rpred 
 |-  ( ph -> T e. RR )
19 18 recnd 
 |-  ( ph -> T e. CC )
20 19 adantr 
 |-  ( ( ph /\ j e. NN ) -> T e. CC )
21 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
22 21 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. NN0 )
23 20 22 expcld 
 |-  ( ( ph /\ j e. NN ) -> ( T ^ j ) e. CC )
24 nnne0 
 |-  ( j e. NN -> j =/= 0 )
25 24 adantl 
 |-  ( ( ph /\ j e. NN ) -> j =/= 0 )
26 15 17 23 25 div32d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( T ^ j ) ) = ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) )
27 11 20 pncan2d 
 |-  ( ( ph /\ j e. NN ) -> ( ( 1 + T ) - 1 ) = T )
28 27 eqcomd 
 |-  ( ( ph /\ j e. NN ) -> T = ( ( 1 + T ) - 1 ) )
29 28 oveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( T ^ j ) = ( ( ( 1 + T ) - 1 ) ^ j ) )
30 29 oveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( T ^ j ) ) = ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( ( ( 1 + T ) - 1 ) ^ j ) ) )
31 26 30 eqtr3d 
 |-  ( ( ph /\ j e. NN ) -> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) = ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( ( ( 1 + T ) - 1 ) ^ j ) ) )
32 31 mpteq2dva 
 |-  ( 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 ) ) ) )
33 10 32 eqtrd 
 |-  ( ph -> D = ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( ( ( 1 + T ) - 1 ) ^ j ) ) ) )
34 33 seqeq3d 
 |-  ( ph -> seq 1 ( + , D ) = seq 1 ( + , ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( ( ( 1 + T ) - 1 ) ^ j ) ) ) ) )
35 1cnd 
 |-  ( ph -> 1 e. CC )
36 35 19 addcld 
 |-  ( ph -> ( 1 + T ) e. CC )
37 eqid 
 |-  ( abs o. - ) = ( abs o. - )
38 37 cnmetdval 
 |-  ( ( 1 e. CC /\ ( 1 + T ) e. CC ) -> ( 1 ( abs o. - ) ( 1 + T ) ) = ( abs ` ( 1 - ( 1 + T ) ) ) )
39 35 36 38 syl2anc 
 |-  ( ph -> ( 1 ( abs o. - ) ( 1 + T ) ) = ( abs ` ( 1 - ( 1 + T ) ) ) )
40 1m1e0 
 |-  ( 1 - 1 ) = 0
41 40 a1i 
 |-  ( ph -> ( 1 - 1 ) = 0 )
42 41 oveq1d 
 |-  ( ph -> ( ( 1 - 1 ) - T ) = ( 0 - T ) )
43 35 35 19 subsub4d 
 |-  ( ph -> ( ( 1 - 1 ) - T ) = ( 1 - ( 1 + T ) ) )
44 df-neg 
 |-  -u T = ( 0 - T )
45 44 eqcomi 
 |-  ( 0 - T ) = -u T
46 45 a1i 
 |-  ( ph -> ( 0 - T ) = -u T )
47 42 43 46 3eqtr3d 
 |-  ( ph -> ( 1 - ( 1 + T ) ) = -u T )
48 47 fveq2d 
 |-  ( ph -> ( abs ` ( 1 - ( 1 + T ) ) ) = ( abs ` -u T ) )
49 19 absnegd 
 |-  ( ph -> ( abs ` -u T ) = ( abs ` T ) )
50 49 7 eqbrtrd 
 |-  ( ph -> ( abs ` -u T ) < 1 )
51 48 50 eqbrtrd 
 |-  ( ph -> ( abs ` ( 1 - ( 1 + T ) ) ) < 1 )
52 39 51 eqbrtrd 
 |-  ( ph -> ( 1 ( abs o. - ) ( 1 + T ) ) < 1 )
53 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
54 53 a1i 
 |-  ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
55 1red 
 |-  ( ph -> 1 e. RR )
56 55 rexrd 
 |-  ( ph -> 1 e. RR* )
57 elbl2 
 |-  ( ( ( ( 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 ) )
58 54 56 35 36 57 syl22anc 
 |-  ( ph -> ( ( 1 + T ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( 1 ( abs o. - ) ( 1 + T ) ) < 1 ) )
59 52 58 mpbird 
 |-  ( ph -> ( 1 + T ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
60 eqid 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
61 60 logtayl2 
 |-  ( ( 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 ) ) )
62 59 61 syl 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) / j ) x. ( ( ( 1 + T ) - 1 ) ^ j ) ) ) ) ~~> ( log ` ( 1 + T ) ) )
63 34 62 eqbrtrd 
 |-  ( ph -> seq 1 ( + , D ) ~~> ( log ` ( 1 + T ) ) )
64 seqex 
 |-  seq 1 ( + , F ) e. _V
65 64 a1i 
 |-  ( ph -> seq 1 ( + , F ) e. _V )
66 2 a1i 
 |-  ( ph -> E = ( j e. NN |-> ( ( T ^ j ) / j ) ) )
67 66 seqeq3d 
 |-  ( ph -> seq 1 ( + , E ) = seq 1 ( + , ( j e. NN |-> ( ( T ^ j ) / j ) ) ) )
68 logtayl 
 |-  ( ( T e. CC /\ ( abs ` T ) < 1 ) -> seq 1 ( + , ( j e. NN |-> ( ( T ^ j ) / j ) ) ) ~~> -u ( log ` ( 1 - T ) ) )
69 19 7 68 syl2anc 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( T ^ j ) / j ) ) ) ~~> -u ( log ` ( 1 - T ) ) )
70 67 69 eqbrtrd 
 |-  ( ph -> seq 1 ( + , E ) ~~> -u ( log ` ( 1 - T ) ) )
71 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
72 71 8 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
73 oveq1 
 |-  ( j = n -> ( j - 1 ) = ( n - 1 ) )
74 73 oveq2d 
 |-  ( j = n -> ( -u 1 ^ ( j - 1 ) ) = ( -u 1 ^ ( n - 1 ) ) )
75 oveq2 
 |-  ( j = n -> ( T ^ j ) = ( T ^ n ) )
76 id 
 |-  ( j = n -> j = n )
77 75 76 oveq12d 
 |-  ( j = n -> ( ( T ^ j ) / j ) = ( ( T ^ n ) / n ) )
78 74 77 oveq12d 
 |-  ( j = n -> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) = ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) )
79 elfznn 
 |-  ( n e. ( 1 ... k ) -> n e. NN )
80 79 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. NN )
81 1cnd 
 |-  ( n e. NN -> 1 e. CC )
82 81 negcld 
 |-  ( n e. NN -> -u 1 e. CC )
83 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
84 82 83 expcld 
 |-  ( n e. NN -> ( -u 1 ^ ( n - 1 ) ) e. CC )
85 80 84 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
86 19 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> T e. CC )
87 80 nnnn0d 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. NN0 )
88 86 87 expcld 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( T ^ n ) e. CC )
89 80 nncnd 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. CC )
90 80 nnne0d 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n =/= 0 )
91 88 89 90 divcld 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( ( T ^ n ) / n ) e. CC )
92 85 91 mulcld 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) e. CC )
93 1 78 80 92 fvmptd3 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( D ` n ) = ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) )
94 93 92 eqeltrd 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( D ` n ) e. CC )
95 addcl 
 |-  ( ( n e. CC /\ i e. CC ) -> ( n + i ) e. CC )
96 95 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( n + i ) e. CC )
97 72 94 96 seqcl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , D ) ` k ) e. CC )
98 2 77 80 91 fvmptd3 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( E ` n ) = ( ( T ^ n ) / n ) )
99 98 91 eqeltrd 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( E ` n ) e. CC )
100 72 99 96 seqcl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , E ) ` k ) e. CC )
101 simpll 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ph )
102 78 77 oveq12d 
 |-  ( j = n -> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) + ( ( T ^ j ) / j ) ) = ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) )
103 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
104 84 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
105 19 adantr 
 |-  ( ( ph /\ n e. NN ) -> T e. CC )
106 103 nnnn0d 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
107 105 106 expcld 
 |-  ( ( ph /\ n e. NN ) -> ( T ^ n ) e. CC )
108 103 nncnd 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
109 103 nnne0d 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
110 107 108 109 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( T ^ n ) / n ) e. CC )
111 104 110 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) e. CC )
112 111 110 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) e. CC )
113 3 102 103 112 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) )
114 1 78 103 111 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) )
115 114 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) = ( D ` n ) )
116 2 77 103 110 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) = ( ( T ^ n ) / n ) )
117 116 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( T ^ n ) / n ) = ( E ` n ) )
118 115 117 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) = ( ( D ` n ) + ( E ` n ) ) )
119 113 118 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( D ` n ) + ( E ` n ) ) )
120 101 80 119 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( F ` n ) = ( ( D ` n ) + ( E ` n ) ) )
121 72 94 99 120 seradd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) = ( ( seq 1 ( + , D ) ` k ) + ( seq 1 ( + , E ) ` k ) ) )
122 8 9 63 65 70 97 100 121 climadd 
 |-  ( ph -> seq 1 ( + , F ) ~~> ( ( log ` ( 1 + T ) ) + -u ( log ` ( 1 - T ) ) ) )
123 1rp 
 |-  1 e. RR+
124 123 a1i 
 |-  ( ph -> 1 e. RR+ )
125 124 6 rpaddcld 
 |-  ( ph -> ( 1 + T ) e. RR+ )
126 125 rpne0d 
 |-  ( ph -> ( 1 + T ) =/= 0 )
127 36 126 logcld 
 |-  ( ph -> ( log ` ( 1 + T ) ) e. CC )
128 35 19 subcld 
 |-  ( ph -> ( 1 - T ) e. CC )
129 18 55 absltd 
 |-  ( ph -> ( ( abs ` T ) < 1 <-> ( -u 1 < T /\ T < 1 ) ) )
130 7 129 mpbid 
 |-  ( ph -> ( -u 1 < T /\ T < 1 ) )
131 130 simprd 
 |-  ( ph -> T < 1 )
132 18 131 gtned 
 |-  ( ph -> 1 =/= T )
133 35 19 132 subne0d 
 |-  ( ph -> ( 1 - T ) =/= 0 )
134 128 133 logcld 
 |-  ( ph -> ( log ` ( 1 - T ) ) e. CC )
135 127 134 negsubd 
 |-  ( ph -> ( ( log ` ( 1 + T ) ) + -u ( log ` ( 1 - T ) ) ) = ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) )
136 122 135 breqtrd 
 |-  ( ph -> seq 1 ( + , F ) ~~> ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) )
137 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
138 0zd 
 |-  ( ph -> 0 e. ZZ )
139 2nn0 
 |-  2 e. NN0
140 139 a1i 
 |-  ( j e. NN0 -> 2 e. NN0 )
141 id 
 |-  ( j e. NN0 -> j e. NN0 )
142 140 141 nn0mulcld 
 |-  ( j e. NN0 -> ( 2 x. j ) e. NN0 )
143 nn0p1nn 
 |-  ( ( 2 x. j ) e. NN0 -> ( ( 2 x. j ) + 1 ) e. NN )
144 142 143 syl 
 |-  ( j e. NN0 -> ( ( 2 x. j ) + 1 ) e. NN )
145 5 144 fmpti 
 |-  G : NN0 --> NN
146 145 a1i 
 |-  ( ph -> G : NN0 --> NN )
147 2re 
 |-  2 e. RR
148 147 a1i 
 |-  ( k e. NN0 -> 2 e. RR )
149 nn0re 
 |-  ( k e. NN0 -> k e. RR )
150 148 149 remulcld 
 |-  ( k e. NN0 -> ( 2 x. k ) e. RR )
151 1red 
 |-  ( k e. NN0 -> 1 e. RR )
152 149 151 readdcld 
 |-  ( k e. NN0 -> ( k + 1 ) e. RR )
153 148 152 remulcld 
 |-  ( k e. NN0 -> ( 2 x. ( k + 1 ) ) e. RR )
154 2rp 
 |-  2 e. RR+
155 154 a1i 
 |-  ( k e. NN0 -> 2 e. RR+ )
156 149 ltp1d 
 |-  ( k e. NN0 -> k < ( k + 1 ) )
157 149 152 155 156 ltmul2dd 
 |-  ( k e. NN0 -> ( 2 x. k ) < ( 2 x. ( k + 1 ) ) )
158 150 153 151 157 ltadd1dd 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) < ( ( 2 x. ( k + 1 ) ) + 1 ) )
159 5 a1i 
 |-  ( k e. NN0 -> G = ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) ) )
160 simpr 
 |-  ( ( k e. NN0 /\ j = k ) -> j = k )
161 160 oveq2d 
 |-  ( ( k e. NN0 /\ j = k ) -> ( 2 x. j ) = ( 2 x. k ) )
162 161 oveq1d 
 |-  ( ( k e. NN0 /\ j = k ) -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. k ) + 1 ) )
163 id 
 |-  ( k e. NN0 -> k e. NN0 )
164 2cnd 
 |-  ( k e. NN0 -> 2 e. CC )
165 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
166 164 165 mulcld 
 |-  ( k e. NN0 -> ( 2 x. k ) e. CC )
167 1cnd 
 |-  ( k e. NN0 -> 1 e. CC )
168 166 167 addcld 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. CC )
169 159 162 163 168 fvmptd 
 |-  ( k e. NN0 -> ( G ` k ) = ( ( 2 x. k ) + 1 ) )
170 simpr 
 |-  ( ( k e. NN0 /\ j = ( k + 1 ) ) -> j = ( k + 1 ) )
171 170 oveq2d 
 |-  ( ( k e. NN0 /\ j = ( k + 1 ) ) -> ( 2 x. j ) = ( 2 x. ( k + 1 ) ) )
172 171 oveq1d 
 |-  ( ( k e. NN0 /\ j = ( k + 1 ) ) -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. ( k + 1 ) ) + 1 ) )
173 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
174 165 167 addcld 
 |-  ( k e. NN0 -> ( k + 1 ) e. CC )
175 164 174 mulcld 
 |-  ( k e. NN0 -> ( 2 x. ( k + 1 ) ) e. CC )
176 175 167 addcld 
 |-  ( k e. NN0 -> ( ( 2 x. ( k + 1 ) ) + 1 ) e. CC )
177 159 172 173 176 fvmptd 
 |-  ( k e. NN0 -> ( G ` ( k + 1 ) ) = ( ( 2 x. ( k + 1 ) ) + 1 ) )
178 158 169 177 3brtr4d 
 |-  ( k e. NN0 -> ( G ` k ) < ( G ` ( k + 1 ) ) )
179 178 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
180 eldifi 
 |-  ( n e. ( NN \ ran G ) -> n e. NN )
181 180 adantl 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> n e. NN )
182 1cnd 
 |-  ( n e. ( NN \ ran G ) -> 1 e. CC )
183 182 negcld 
 |-  ( n e. ( NN \ ran G ) -> -u 1 e. CC )
184 180 83 syl 
 |-  ( n e. ( NN \ ran G ) -> ( n - 1 ) e. NN0 )
185 183 184 expcld 
 |-  ( n e. ( NN \ ran G ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
186 185 adantl 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
187 19 adantr 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> T e. CC )
188 181 nnnn0d 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> n e. NN0 )
189 187 188 expcld 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( T ^ n ) e. CC )
190 181 nncnd 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> n e. CC )
191 181 nnne0d 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> n =/= 0 )
192 189 190 191 divcld 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( T ^ n ) / n ) e. CC )
193 186 192 mulcld 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) e. CC )
194 193 192 addcld 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) e. CC )
195 3 102 181 194 fvmptd3 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( F ` n ) = ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) )
196 eldifn 
 |-  ( n e. ( NN \ ran G ) -> -. n e. ran G )
197 0nn0 
 |-  0 e. NN0
198 1nn0 
 |-  1 e. NN0
199 139 198 num0h 
 |-  1 = ( ( 2 x. 0 ) + 1 )
200 oveq2 
 |-  ( j = 0 -> ( 2 x. j ) = ( 2 x. 0 ) )
201 200 oveq1d 
 |-  ( j = 0 -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. 0 ) + 1 ) )
202 201 eqeq2d 
 |-  ( j = 0 -> ( 1 = ( ( 2 x. j ) + 1 ) <-> 1 = ( ( 2 x. 0 ) + 1 ) ) )
203 202 rspcev 
 |-  ( ( 0 e. NN0 /\ 1 = ( ( 2 x. 0 ) + 1 ) ) -> E. j e. NN0 1 = ( ( 2 x. j ) + 1 ) )
204 197 199 203 mp2an 
 |-  E. j e. NN0 1 = ( ( 2 x. j ) + 1 )
205 ax-1cn 
 |-  1 e. CC
206 5 elrnmpt 
 |-  ( 1 e. CC -> ( 1 e. ran G <-> E. j e. NN0 1 = ( ( 2 x. j ) + 1 ) ) )
207 205 206 ax-mp 
 |-  ( 1 e. ran G <-> E. j e. NN0 1 = ( ( 2 x. j ) + 1 ) )
208 204 207 mpbir 
 |-  1 e. ran G
209 208 a1i 
 |-  ( n = 1 -> 1 e. ran G )
210 eleq1 
 |-  ( n = 1 -> ( n e. ran G <-> 1 e. ran G ) )
211 209 210 mpbird 
 |-  ( n = 1 -> n e. ran G )
212 196 211 nsyl 
 |-  ( n e. ( NN \ ran G ) -> -. n = 1 )
213 nn1m1nn 
 |-  ( n e. NN -> ( n = 1 \/ ( n - 1 ) e. NN ) )
214 180 213 syl 
 |-  ( n e. ( NN \ ran G ) -> ( n = 1 \/ ( n - 1 ) e. NN ) )
215 214 ord 
 |-  ( n e. ( NN \ ran G ) -> ( -. n = 1 -> ( n - 1 ) e. NN ) )
216 212 215 mpd 
 |-  ( n e. ( NN \ ran G ) -> ( n - 1 ) e. NN )
217 nfcv 
 |-  F/_ j NN
218 nfmpt1 
 |-  F/_ j ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) )
219 5 218 nfcxfr 
 |-  F/_ j G
220 219 nfrn 
 |-  F/_ j ran G
221 217 220 nfdif 
 |-  F/_ j ( NN \ ran G )
222 221 nfcri 
 |-  F/ j n e. ( NN \ ran G )
223 5 elrnmpt 
 |-  ( n e. ( NN \ ran G ) -> ( n e. ran G <-> E. j e. NN0 n = ( ( 2 x. j ) + 1 ) ) )
224 196 223 mtbid 
 |-  ( n e. ( NN \ ran G ) -> -. E. j e. NN0 n = ( ( 2 x. j ) + 1 ) )
225 ralnex 
 |-  ( A. j e. NN0 -. n = ( ( 2 x. j ) + 1 ) <-> -. E. j e. NN0 n = ( ( 2 x. j ) + 1 ) )
226 224 225 sylibr 
 |-  ( n e. ( NN \ ran G ) -> A. j e. NN0 -. n = ( ( 2 x. j ) + 1 ) )
227 226 r19.21bi 
 |-  ( ( n e. ( NN \ ran G ) /\ j e. NN0 ) -> -. n = ( ( 2 x. j ) + 1 ) )
228 227 neqned 
 |-  ( ( n e. ( NN \ ran G ) /\ j e. NN0 ) -> n =/= ( ( 2 x. j ) + 1 ) )
229 228 necomd 
 |-  ( ( n e. ( NN \ ran G ) /\ j e. NN0 ) -> ( ( 2 x. j ) + 1 ) =/= n )
230 229 adantlr 
 |-  ( ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) /\ j e. NN0 ) -> ( ( 2 x. j ) + 1 ) =/= n )
231 simplr 
 |-  ( ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) /\ -. j e. NN0 ) -> j e. ZZ )
232 simpr 
 |-  ( ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) /\ -. j e. NN0 ) -> -. j e. NN0 )
233 180 ad2antrr 
 |-  ( ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) /\ -. j e. NN0 ) -> n e. NN )
234 147 a1i 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 2 e. RR )
235 simpl 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> j e. ZZ )
236 235 zred 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> j e. RR )
237 234 236 remulcld 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( 2 x. j ) e. RR )
238 0red 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 0 e. RR )
239 1red 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 1 e. RR )
240 2cnd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 2 e. CC )
241 236 recnd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> j e. CC )
242 240 241 mulcomd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( 2 x. j ) = ( j x. 2 ) )
243 simpr 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> -. j e. NN0 )
244 elnn0z 
 |-  ( j e. NN0 <-> ( j e. ZZ /\ 0 <_ j ) )
245 243 244 sylnib 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> -. ( j e. ZZ /\ 0 <_ j ) )
246 nan 
 |-  ( ( ( j e. ZZ /\ -. j e. NN0 ) -> -. ( j e. ZZ /\ 0 <_ j ) ) <-> ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ j e. ZZ ) -> -. 0 <_ j ) )
247 245 246 mpbi 
 |-  ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ j e. ZZ ) -> -. 0 <_ j )
248 247 anabss1 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> -. 0 <_ j )
249 236 238 ltnled 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( j < 0 <-> -. 0 <_ j ) )
250 248 249 mpbird 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> j < 0 )
251 154 a1i 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 2 e. RR+ )
252 251 rpregt0d 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( 2 e. RR /\ 0 < 2 ) )
253 mulltgt0 
 |-  ( ( ( j e. RR /\ j < 0 ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( j x. 2 ) < 0 )
254 236 250 252 253 syl21anc 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( j x. 2 ) < 0 )
255 242 254 eqbrtrd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( 2 x. j ) < 0 )
256 237 238 239 255 ltadd1dd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( ( 2 x. j ) + 1 ) < ( 0 + 1 ) )
257 1cnd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> 1 e. CC )
258 257 addlidd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( 0 + 1 ) = 1 )
259 256 258 breqtrd 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( ( 2 x. j ) + 1 ) < 1 )
260 237 239 readdcld 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( ( 2 x. j ) + 1 ) e. RR )
261 260 239 ltnled 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> ( ( ( 2 x. j ) + 1 ) < 1 <-> -. 1 <_ ( ( 2 x. j ) + 1 ) ) )
262 259 261 mpbid 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> -. 1 <_ ( ( 2 x. j ) + 1 ) )
263 nnge1 
 |-  ( ( ( 2 x. j ) + 1 ) e. NN -> 1 <_ ( ( 2 x. j ) + 1 ) )
264 262 263 nsyl 
 |-  ( ( j e. ZZ /\ -. j e. NN0 ) -> -. ( ( 2 x. j ) + 1 ) e. NN )
265 264 adantr 
 |-  ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ n e. NN ) -> -. ( ( 2 x. j ) + 1 ) e. NN )
266 simpr 
 |-  ( ( n e. NN /\ ( ( 2 x. j ) + 1 ) = n ) -> ( ( 2 x. j ) + 1 ) = n )
267 simpl 
 |-  ( ( n e. NN /\ ( ( 2 x. j ) + 1 ) = n ) -> n e. NN )
268 266 267 eqeltrd 
 |-  ( ( n e. NN /\ ( ( 2 x. j ) + 1 ) = n ) -> ( ( 2 x. j ) + 1 ) e. NN )
269 268 adantll 
 |-  ( ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ n e. NN ) /\ ( ( 2 x. j ) + 1 ) = n ) -> ( ( 2 x. j ) + 1 ) e. NN )
270 265 269 mtand 
 |-  ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ n e. NN ) -> -. ( ( 2 x. j ) + 1 ) = n )
271 270 neqned 
 |-  ( ( ( j e. ZZ /\ -. j e. NN0 ) /\ n e. NN ) -> ( ( 2 x. j ) + 1 ) =/= n )
272 231 232 233 271 syl21anc 
 |-  ( ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) /\ -. j e. NN0 ) -> ( ( 2 x. j ) + 1 ) =/= n )
273 230 272 pm2.61dan 
 |-  ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) -> ( ( 2 x. j ) + 1 ) =/= n )
274 273 neneqd 
 |-  ( ( n e. ( NN \ ran G ) /\ j e. ZZ ) -> -. ( ( 2 x. j ) + 1 ) = n )
275 274 ex 
 |-  ( n e. ( NN \ ran G ) -> ( j e. ZZ -> -. ( ( 2 x. j ) + 1 ) = n ) )
276 222 275 ralrimi 
 |-  ( n e. ( NN \ ran G ) -> A. j e. ZZ -. ( ( 2 x. j ) + 1 ) = n )
277 ralnex 
 |-  ( A. j e. ZZ -. ( ( 2 x. j ) + 1 ) = n <-> -. E. j e. ZZ ( ( 2 x. j ) + 1 ) = n )
278 276 277 sylib 
 |-  ( n e. ( NN \ ran G ) -> -. E. j e. ZZ ( ( 2 x. j ) + 1 ) = n )
279 180 nnzd 
 |-  ( n e. ( NN \ ran G ) -> n e. ZZ )
280 odd2np1 
 |-  ( n e. ZZ -> ( -. 2 || n <-> E. j e. ZZ ( ( 2 x. j ) + 1 ) = n ) )
281 279 280 syl 
 |-  ( n e. ( NN \ ran G ) -> ( -. 2 || n <-> E. j e. ZZ ( ( 2 x. j ) + 1 ) = n ) )
282 278 281 mtbird 
 |-  ( n e. ( NN \ ran G ) -> -. -. 2 || n )
283 282 notnotrd 
 |-  ( n e. ( NN \ ran G ) -> 2 || n )
284 180 nncnd 
 |-  ( n e. ( NN \ ran G ) -> n e. CC )
285 284 182 npcand 
 |-  ( n e. ( NN \ ran G ) -> ( ( n - 1 ) + 1 ) = n )
286 283 285 breqtrrd 
 |-  ( n e. ( NN \ ran G ) -> 2 || ( ( n - 1 ) + 1 ) )
287 184 nn0zd 
 |-  ( n e. ( NN \ ran G ) -> ( n - 1 ) e. ZZ )
288 oddp1even 
 |-  ( ( n - 1 ) e. ZZ -> ( -. 2 || ( n - 1 ) <-> 2 || ( ( n - 1 ) + 1 ) ) )
289 287 288 syl 
 |-  ( n e. ( NN \ ran G ) -> ( -. 2 || ( n - 1 ) <-> 2 || ( ( n - 1 ) + 1 ) ) )
290 286 289 mpbird 
 |-  ( n e. ( NN \ ran G ) -> -. 2 || ( n - 1 ) )
291 oexpneg 
 |-  ( ( 1 e. CC /\ ( n - 1 ) e. NN /\ -. 2 || ( n - 1 ) ) -> ( -u 1 ^ ( n - 1 ) ) = -u ( 1 ^ ( n - 1 ) ) )
292 182 216 290 291 syl3anc 
 |-  ( n e. ( NN \ ran G ) -> ( -u 1 ^ ( n - 1 ) ) = -u ( 1 ^ ( n - 1 ) ) )
293 1exp 
 |-  ( ( n - 1 ) e. ZZ -> ( 1 ^ ( n - 1 ) ) = 1 )
294 287 293 syl 
 |-  ( n e. ( NN \ ran G ) -> ( 1 ^ ( n - 1 ) ) = 1 )
295 294 negeqd 
 |-  ( n e. ( NN \ ran G ) -> -u ( 1 ^ ( n - 1 ) ) = -u 1 )
296 292 295 eqtrd 
 |-  ( n e. ( NN \ ran G ) -> ( -u 1 ^ ( n - 1 ) ) = -u 1 )
297 296 adantl 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( -u 1 ^ ( n - 1 ) ) = -u 1 )
298 297 oveq1d 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( T ^ n ) / n ) ) = ( -u 1 x. ( ( T ^ n ) / n ) ) )
299 298 oveq1d 
 |-  ( ( 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 ) ) )
300 192 mulm1d 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( -u 1 x. ( ( T ^ n ) / n ) ) = -u ( ( T ^ n ) / n ) )
301 300 oveq1d 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( -u 1 x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) = ( -u ( ( T ^ n ) / n ) + ( ( T ^ n ) / n ) ) )
302 192 negcld 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> -u ( ( T ^ n ) / n ) e. CC )
303 302 192 addcomd 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( -u ( ( T ^ n ) / n ) + ( ( T ^ n ) / n ) ) = ( ( ( T ^ n ) / n ) + -u ( ( T ^ n ) / n ) ) )
304 192 negidd 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( ( T ^ n ) / n ) + -u ( ( T ^ n ) / n ) ) = 0 )
305 301 303 304 3eqtrd 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( ( -u 1 x. ( ( T ^ n ) / n ) ) + ( ( T ^ n ) / n ) ) = 0 )
306 195 299 305 3eqtrd 
 |-  ( ( ph /\ n e. ( NN \ ran G ) ) -> ( F ` n ) = 0 )
307 113 112 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. CC )
308 3 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> F = ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) + ( ( T ^ j ) / j ) ) ) )
309 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( ( 2 x. k ) + 1 ) ) -> j = ( ( 2 x. k ) + 1 ) )
310 309 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( ( 2 x. k ) + 1 ) ) -> ( j - 1 ) = ( ( ( 2 x. k ) + 1 ) - 1 ) )
311 310 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( ( 2 x. k ) + 1 ) ) -> ( -u 1 ^ ( j - 1 ) ) = ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) )
312 309 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( ( 2 x. k ) + 1 ) ) -> ( T ^ j ) = ( T ^ ( ( 2 x. k ) + 1 ) ) )
313 312 309 oveq12d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( ( 2 x. k ) + 1 ) ) -> ( ( T ^ j ) / j ) = ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) )
314 311 313 oveq12d 
 |-  ( ( ( 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 ) ) ) )
315 314 313 oveq12d 
 |-  ( ( ( 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 ) ) ) )
316 139 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 2 e. NN0 )
317 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
318 316 317 nn0mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
319 nn0p1nn 
 |-  ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN )
320 318 319 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. NN )
321 167 negcld 
 |-  ( k e. NN0 -> -u 1 e. CC )
322 166 167 pncand 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
323 139 a1i 
 |-  ( k e. NN0 -> 2 e. NN0 )
324 323 163 nn0mulcld 
 |-  ( k e. NN0 -> ( 2 x. k ) e. NN0 )
325 322 324 eqeltrd 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) - 1 ) e. NN0 )
326 321 325 expcld 
 |-  ( k e. NN0 -> ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) e. CC )
327 326 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) e. CC )
328 19 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> T e. CC )
329 198 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 1 e. NN0 )
330 318 329 nn0addcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. NN0 )
331 328 330 expcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( T ^ ( ( 2 x. k ) + 1 ) ) e. CC )
332 2cnd 
 |-  ( ( ph /\ k e. NN0 ) -> 2 e. CC )
333 165 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. CC )
334 332 333 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. CC )
335 1cnd 
 |-  ( ( ph /\ k e. NN0 ) -> 1 e. CC )
336 334 335 addcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. CC )
337 0red 
 |-  ( ( ph /\ k e. NN0 ) -> 0 e. RR )
338 147 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 2 e. RR )
339 149 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. RR )
340 338 339 remulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. RR )
341 1red 
 |-  ( ( ph /\ k e. NN0 ) -> 1 e. RR )
342 0le2 
 |-  0 <_ 2
343 342 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ 2 )
344 317 nn0ge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ k )
345 338 339 343 344 mulge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( 2 x. k ) )
346 0lt1 
 |-  0 < 1
347 346 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 0 < 1 )
348 340 341 345 347 addgegt0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 < ( ( 2 x. k ) + 1 ) )
349 337 348 gtned 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) =/= 0 )
350 331 336 349 divcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) e. CC )
351 327 350 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) x. ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) e. CC )
352 351 350 addcld 
 |-  ( ( 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 )
353 308 315 320 352 fvmptd 
 |-  ( ( 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 ) ) ) )
354 322 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
355 354 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) = ( -u 1 ^ ( 2 x. k ) ) )
356 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
357 m1expeven 
 |-  ( k e. ZZ -> ( -u 1 ^ ( 2 x. k ) ) = 1 )
358 356 357 syl 
 |-  ( k e. NN0 -> ( -u 1 ^ ( 2 x. k ) ) = 1 )
359 358 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( -u 1 ^ ( 2 x. k ) ) = 1 )
360 355 359 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( -u 1 ^ ( ( ( 2 x. k ) + 1 ) - 1 ) ) = 1 )
361 360 oveq1d 
 |-  ( ( 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 ) ) ) )
362 350 mullidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) = ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) )
363 361 362 eqtrd 
 |-  ( ( 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 ) ) )
364 363 oveq1d 
 |-  ( ( 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 ) ) ) )
365 350 2timesd 
 |-  ( ( 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 ) ) ) )
366 331 336 349 divrec2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( T ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) = ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( T ^ ( ( 2 x. k ) + 1 ) ) ) )
367 366 oveq2d 
 |-  ( ( 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 ) ) ) ) )
368 364 365 367 3eqtr2d 
 |-  ( ( 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 ) ) ) ) )
369 353 368 eqtr2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( T ^ ( ( 2 x. k ) + 1 ) ) ) ) = ( F ` ( ( 2 x. k ) + 1 ) ) )
370 4 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( T ^ ( ( 2 x. j ) + 1 ) ) ) ) ) )
371 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> j = k )
372 371 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( 2 x. j ) = ( 2 x. k ) )
373 372 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. k ) + 1 ) )
374 373 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
375 373 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( T ^ ( ( 2 x. j ) + 1 ) ) = ( T ^ ( ( 2 x. k ) + 1 ) ) )
376 374 375 oveq12d 
 |-  ( ( ( 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 ) ) ) )
377 376 oveq2d 
 |-  ( ( ( 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 ) ) ) ) )
378 336 349 reccld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. CC )
379 378 331 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( T ^ ( ( 2 x. k ) + 1 ) ) ) e. CC )
380 332 379 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( T ^ ( ( 2 x. k ) + 1 ) ) ) ) e. CC )
381 370 377 317 380 fvmptd 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( T ^ ( ( 2 x. k ) + 1 ) ) ) ) )
382 198 a1i 
 |-  ( k e. NN0 -> 1 e. NN0 )
383 324 382 nn0addcld 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN0 )
384 159 162 163 383 fvmptd 
 |-  ( k e. NN0 -> ( G ` k ) = ( ( 2 x. k ) + 1 ) )
385 384 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) = ( ( 2 x. k ) + 1 ) )
386 385 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( G ` k ) ) = ( F ` ( ( 2 x. k ) + 1 ) ) )
387 369 381 386 3eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
388 137 8 138 9 146 179 306 307 387 isercoll2 
 |-  ( ph -> ( seq 0 ( + , H ) ~~> ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) <-> seq 1 ( + , F ) ~~> ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) ) )
389 136 388 mpbird 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) )
390 55 18 resubcld 
 |-  ( ph -> ( 1 - T ) e. RR )
391 19 subidd 
 |-  ( ph -> ( T - T ) = 0 )
392 391 eqcomd 
 |-  ( ph -> 0 = ( T - T ) )
393 18 55 18 131 ltsub1dd 
 |-  ( ph -> ( T - T ) < ( 1 - T ) )
394 392 393 eqbrtrd 
 |-  ( ph -> 0 < ( 1 - T ) )
395 390 394 elrpd 
 |-  ( ph -> ( 1 - T ) e. RR+ )
396 125 395 relogdivd 
 |-  ( ph -> ( log ` ( ( 1 + T ) / ( 1 - T ) ) ) = ( ( log ` ( 1 + T ) ) - ( log ` ( 1 - T ) ) ) )
397 389 396 breqtrrd 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( log ` ( ( 1 + T ) / ( 1 - T ) ) ) )