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 ) ) ) ) |