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 addid2d
 |-  ( ( 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 mulid2d
 |-  ( ( 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 ) ) ) )