Step |
Hyp |
Ref |
Expression |
1 |
|
leibpi.1 |
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) |
2 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
3 |
|
0zd |
|- ( T. -> 0 e. ZZ ) |
4 |
|
eqidd |
|- ( ( T. /\ j e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
5 |
|
0cnd |
|- ( ( k e. NN0 /\ ( k = 0 \/ 2 || k ) ) -> 0 e. CC ) |
6 |
|
ioran |
|- ( -. ( k = 0 \/ 2 || k ) <-> ( -. k = 0 /\ -. 2 || k ) ) |
7 |
|
neg1rr |
|- -u 1 e. RR |
8 |
|
leibpilem1 |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( k e. NN /\ ( ( k - 1 ) / 2 ) e. NN0 ) ) |
9 |
8
|
simprd |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( k - 1 ) / 2 ) e. NN0 ) |
10 |
|
reexpcl |
|- ( ( -u 1 e. RR /\ ( ( k - 1 ) / 2 ) e. NN0 ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. RR ) |
11 |
7 9 10
|
sylancr |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. RR ) |
12 |
8
|
simpld |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> k e. NN ) |
13 |
11 12
|
nndivred |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. RR ) |
14 |
13
|
recnd |
|- ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. CC ) |
15 |
6 14
|
sylan2b |
|- ( ( k e. NN0 /\ -. ( k = 0 \/ 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. CC ) |
16 |
5 15
|
ifclda |
|- ( k e. NN0 -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) e. CC ) |
17 |
16
|
adantl |
|- ( ( T. /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) e. CC ) |
18 |
17
|
fmpttd |
|- ( T. -> ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) : NN0 --> CC ) |
19 |
18
|
ffvelrnda |
|- ( ( T. /\ j e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) e. CC ) |
20 |
|
2nn0 |
|- 2 e. NN0 |
21 |
20
|
a1i |
|- ( T. -> 2 e. NN0 ) |
22 |
|
nn0mulcl |
|- ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 ) |
23 |
21 22
|
sylan |
|- ( ( T. /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 ) |
24 |
|
nn0p1nn |
|- ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN ) |
25 |
23 24
|
syl |
|- ( ( T. /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) e. NN ) |
26 |
25
|
nnrecred |
|- ( ( T. /\ n e. NN0 ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR ) |
27 |
26
|
fmpttd |
|- ( T. -> ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) : NN0 --> RR ) |
28 |
|
nn0mulcl |
|- ( ( 2 e. NN0 /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 ) |
29 |
21 28
|
sylan |
|- ( ( T. /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 ) |
30 |
29
|
nn0red |
|- ( ( T. /\ k e. NN0 ) -> ( 2 x. k ) e. RR ) |
31 |
|
peano2nn0 |
|- ( k e. NN0 -> ( k + 1 ) e. NN0 ) |
32 |
31
|
adantl |
|- ( ( T. /\ k e. NN0 ) -> ( k + 1 ) e. NN0 ) |
33 |
|
nn0mulcl |
|- ( ( 2 e. NN0 /\ ( k + 1 ) e. NN0 ) -> ( 2 x. ( k + 1 ) ) e. NN0 ) |
34 |
20 32 33
|
sylancr |
|- ( ( T. /\ k e. NN0 ) -> ( 2 x. ( k + 1 ) ) e. NN0 ) |
35 |
34
|
nn0red |
|- ( ( T. /\ k e. NN0 ) -> ( 2 x. ( k + 1 ) ) e. RR ) |
36 |
|
1red |
|- ( ( T. /\ k e. NN0 ) -> 1 e. RR ) |
37 |
|
nn0re |
|- ( k e. NN0 -> k e. RR ) |
38 |
37
|
adantl |
|- ( ( T. /\ k e. NN0 ) -> k e. RR ) |
39 |
38
|
lep1d |
|- ( ( T. /\ k e. NN0 ) -> k <_ ( k + 1 ) ) |
40 |
|
peano2re |
|- ( k e. RR -> ( k + 1 ) e. RR ) |
41 |
38 40
|
syl |
|- ( ( T. /\ k e. NN0 ) -> ( k + 1 ) e. RR ) |
42 |
|
2re |
|- 2 e. RR |
43 |
42
|
a1i |
|- ( ( T. /\ k e. NN0 ) -> 2 e. RR ) |
44 |
|
2pos |
|- 0 < 2 |
45 |
44
|
a1i |
|- ( ( T. /\ k e. NN0 ) -> 0 < 2 ) |
46 |
|
lemul2 |
|- ( ( k e. RR /\ ( k + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( k <_ ( k + 1 ) <-> ( 2 x. k ) <_ ( 2 x. ( k + 1 ) ) ) ) |
47 |
38 41 43 45 46
|
syl112anc |
|- ( ( T. /\ k e. NN0 ) -> ( k <_ ( k + 1 ) <-> ( 2 x. k ) <_ ( 2 x. ( k + 1 ) ) ) ) |
48 |
39 47
|
mpbid |
|- ( ( T. /\ k e. NN0 ) -> ( 2 x. k ) <_ ( 2 x. ( k + 1 ) ) ) |
49 |
30 35 36 48
|
leadd1dd |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) <_ ( ( 2 x. ( k + 1 ) ) + 1 ) ) |
50 |
|
nn0p1nn |
|- ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN ) |
51 |
29 50
|
syl |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. NN ) |
52 |
51
|
nnred |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. RR ) |
53 |
51
|
nngt0d |
|- ( ( T. /\ k e. NN0 ) -> 0 < ( ( 2 x. k ) + 1 ) ) |
54 |
|
nn0p1nn |
|- ( ( 2 x. ( k + 1 ) ) e. NN0 -> ( ( 2 x. ( k + 1 ) ) + 1 ) e. NN ) |
55 |
34 54
|
syl |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. ( k + 1 ) ) + 1 ) e. NN ) |
56 |
55
|
nnred |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. ( k + 1 ) ) + 1 ) e. RR ) |
57 |
55
|
nngt0d |
|- ( ( T. /\ k e. NN0 ) -> 0 < ( ( 2 x. ( k + 1 ) ) + 1 ) ) |
58 |
|
lerec |
|- ( ( ( ( ( 2 x. k ) + 1 ) e. RR /\ 0 < ( ( 2 x. k ) + 1 ) ) /\ ( ( ( 2 x. ( k + 1 ) ) + 1 ) e. RR /\ 0 < ( ( 2 x. ( k + 1 ) ) + 1 ) ) ) -> ( ( ( 2 x. k ) + 1 ) <_ ( ( 2 x. ( k + 1 ) ) + 1 ) <-> ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) <_ ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) |
59 |
52 53 56 57 58
|
syl22anc |
|- ( ( T. /\ k e. NN0 ) -> ( ( ( 2 x. k ) + 1 ) <_ ( ( 2 x. ( k + 1 ) ) + 1 ) <-> ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) <_ ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) |
60 |
49 59
|
mpbid |
|- ( ( T. /\ k e. NN0 ) -> ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) <_ ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
61 |
|
oveq2 |
|- ( n = ( k + 1 ) -> ( 2 x. n ) = ( 2 x. ( k + 1 ) ) ) |
62 |
61
|
oveq1d |
|- ( n = ( k + 1 ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. ( k + 1 ) ) + 1 ) ) |
63 |
62
|
oveq2d |
|- ( n = ( k + 1 ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) = ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) ) |
64 |
|
eqid |
|- ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) |
65 |
|
ovex |
|- ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) e. _V |
66 |
63 64 65
|
fvmpt |
|- ( ( k + 1 ) e. NN0 -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` ( k + 1 ) ) = ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) ) |
67 |
32 66
|
syl |
|- ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` ( k + 1 ) ) = ( 1 / ( ( 2 x. ( k + 1 ) ) + 1 ) ) ) |
68 |
|
oveq2 |
|- ( n = k -> ( 2 x. n ) = ( 2 x. k ) ) |
69 |
68
|
oveq1d |
|- ( n = k -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. k ) + 1 ) ) |
70 |
69
|
oveq2d |
|- ( n = k -> ( 1 / ( ( 2 x. n ) + 1 ) ) = ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
71 |
|
ovex |
|- ( 1 / ( ( 2 x. k ) + 1 ) ) e. _V |
72 |
70 64 71
|
fvmpt |
|- ( k e. NN0 -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
73 |
72
|
adantl |
|- ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
74 |
60 67 73
|
3brtr4d |
|- ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` ( k + 1 ) ) <_ ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) ) |
75 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
76 |
|
1zzd |
|- ( T. -> 1 e. ZZ ) |
77 |
|
ax-1cn |
|- 1 e. CC |
78 |
|
divcnv |
|- ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 ) |
79 |
77 78
|
mp1i |
|- ( T. -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 ) |
80 |
|
nn0ex |
|- NN0 e. _V |
81 |
80
|
mptex |
|- ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V |
82 |
81
|
a1i |
|- ( T. -> ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V ) |
83 |
|
oveq2 |
|- ( n = k -> ( 1 / n ) = ( 1 / k ) ) |
84 |
|
eqid |
|- ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) ) |
85 |
|
ovex |
|- ( 1 / k ) e. _V |
86 |
83 84 85
|
fvmpt |
|- ( k e. NN -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) ) |
87 |
86
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) ) |
88 |
|
nnrecre |
|- ( k e. NN -> ( 1 / k ) e. RR ) |
89 |
88
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( 1 / k ) e. RR ) |
90 |
87 89
|
eqeltrd |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) e. RR ) |
91 |
|
nnnn0 |
|- ( k e. NN -> k e. NN0 ) |
92 |
91
|
adantl |
|- ( ( T. /\ k e. NN ) -> k e. NN0 ) |
93 |
92 72
|
syl |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
94 |
91 51
|
sylan2 |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN ) |
95 |
94
|
nnrecred |
|- ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR ) |
96 |
93 95
|
eqeltrd |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) e. RR ) |
97 |
|
nnre |
|- ( k e. NN -> k e. RR ) |
98 |
97
|
adantl |
|- ( ( T. /\ k e. NN ) -> k e. RR ) |
99 |
20 92 28
|
sylancr |
|- ( ( T. /\ k e. NN ) -> ( 2 x. k ) e. NN0 ) |
100 |
99
|
nn0red |
|- ( ( T. /\ k e. NN ) -> ( 2 x. k ) e. RR ) |
101 |
|
peano2re |
|- ( ( 2 x. k ) e. RR -> ( ( 2 x. k ) + 1 ) e. RR ) |
102 |
100 101
|
syl |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. RR ) |
103 |
|
nn0addge1 |
|- ( ( k e. RR /\ k e. NN0 ) -> k <_ ( k + k ) ) |
104 |
98 92 103
|
syl2anc |
|- ( ( T. /\ k e. NN ) -> k <_ ( k + k ) ) |
105 |
98
|
recnd |
|- ( ( T. /\ k e. NN ) -> k e. CC ) |
106 |
105
|
2timesd |
|- ( ( T. /\ k e. NN ) -> ( 2 x. k ) = ( k + k ) ) |
107 |
104 106
|
breqtrrd |
|- ( ( T. /\ k e. NN ) -> k <_ ( 2 x. k ) ) |
108 |
100
|
lep1d |
|- ( ( T. /\ k e. NN ) -> ( 2 x. k ) <_ ( ( 2 x. k ) + 1 ) ) |
109 |
98 100 102 107 108
|
letrd |
|- ( ( T. /\ k e. NN ) -> k <_ ( ( 2 x. k ) + 1 ) ) |
110 |
|
nngt0 |
|- ( k e. NN -> 0 < k ) |
111 |
110
|
adantl |
|- ( ( T. /\ k e. NN ) -> 0 < k ) |
112 |
94
|
nnred |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. RR ) |
113 |
94
|
nngt0d |
|- ( ( T. /\ k e. NN ) -> 0 < ( ( 2 x. k ) + 1 ) ) |
114 |
|
lerec |
|- ( ( ( k e. RR /\ 0 < k ) /\ ( ( ( 2 x. k ) + 1 ) e. RR /\ 0 < ( ( 2 x. k ) + 1 ) ) ) -> ( k <_ ( ( 2 x. k ) + 1 ) <-> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) ) ) |
115 |
98 111 112 113 114
|
syl22anc |
|- ( ( T. /\ k e. NN ) -> ( k <_ ( ( 2 x. k ) + 1 ) <-> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) ) ) |
116 |
109 115
|
mpbid |
|- ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) ) |
117 |
116 93 87
|
3brtr4d |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) <_ ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) |
118 |
94
|
nnrpd |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. RR+ ) |
119 |
118
|
rpreccld |
|- ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR+ ) |
120 |
119
|
rpge0d |
|- ( ( T. /\ k e. NN ) -> 0 <_ ( 1 / ( ( 2 x. k ) + 1 ) ) ) |
121 |
120 93
|
breqtrrd |
|- ( ( T. /\ k e. NN ) -> 0 <_ ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) ) |
122 |
75 76 79 82 90 96 117 121
|
climsqz2 |
|- ( T. -> ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ~~> 0 ) |
123 |
|
neg1cn |
|- -u 1 e. CC |
124 |
123
|
a1i |
|- ( T. -> -u 1 e. CC ) |
125 |
|
expcl |
|- ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC ) |
126 |
124 125
|
sylan |
|- ( ( T. /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC ) |
127 |
51
|
nncnd |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. CC ) |
128 |
51
|
nnne0d |
|- ( ( T. /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) =/= 0 ) |
129 |
126 127 128
|
divrecd |
|- ( ( T. /\ k e. NN0 ) -> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) = ( ( -u 1 ^ k ) x. ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) |
130 |
|
oveq2 |
|- ( n = k -> ( -u 1 ^ n ) = ( -u 1 ^ k ) ) |
131 |
130 69
|
oveq12d |
|- ( n = k -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) = ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) |
132 |
|
eqid |
|- ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) |
133 |
|
ovex |
|- ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) e. _V |
134 |
131 132 133
|
fvmpt |
|- ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) |
135 |
134
|
adantl |
|- ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) |
136 |
73
|
oveq2d |
|- ( ( T. /\ k e. NN0 ) -> ( ( -u 1 ^ k ) x. ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) ) = ( ( -u 1 ^ k ) x. ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) |
137 |
129 135 136
|
3eqtr4d |
|- ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ` k ) = ( ( -u 1 ^ k ) x. ( ( n e. NN0 |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) ` k ) ) ) |
138 |
2 3 27 74 122 137
|
iseralt |
|- ( T. -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) e. dom ~~> ) |
139 |
|
climdm |
|- ( seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) e. dom ~~> <-> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ) |
140 |
138 139
|
sylib |
|- ( T. -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ) |
141 |
|
eqid |
|- ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) = ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) |
142 |
|
fvex |
|- ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) e. _V |
143 |
132 141 142
|
leibpilem2 |
|- ( seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) <-> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ) |
144 |
140 143
|
sylib |
|- ( T. -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ) |
145 |
|
seqex |
|- seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) e. _V |
146 |
145 142
|
breldm |
|- ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) ) ) ) -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) e. dom ~~> ) |
147 |
144 146
|
syl |
|- ( T. -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) e. dom ~~> ) |
148 |
2 3 4 19 147
|
isumclim2 |
|- ( T. -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
149 |
|
eqid |
|- ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) = ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) |
150 |
18 147 149
|
abelth2 |
|- ( T. -> ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) |
151 |
|
nnrp |
|- ( n e. NN -> n e. RR+ ) |
152 |
151
|
adantl |
|- ( ( T. /\ n e. NN ) -> n e. RR+ ) |
153 |
152
|
rpreccld |
|- ( ( T. /\ n e. NN ) -> ( 1 / n ) e. RR+ ) |
154 |
153
|
rpred |
|- ( ( T. /\ n e. NN ) -> ( 1 / n ) e. RR ) |
155 |
153
|
rpge0d |
|- ( ( T. /\ n e. NN ) -> 0 <_ ( 1 / n ) ) |
156 |
|
nnge1 |
|- ( n e. NN -> 1 <_ n ) |
157 |
156
|
adantl |
|- ( ( T. /\ n e. NN ) -> 1 <_ n ) |
158 |
|
nnre |
|- ( n e. NN -> n e. RR ) |
159 |
158
|
adantl |
|- ( ( T. /\ n e. NN ) -> n e. RR ) |
160 |
159
|
recnd |
|- ( ( T. /\ n e. NN ) -> n e. CC ) |
161 |
160
|
mulid1d |
|- ( ( T. /\ n e. NN ) -> ( n x. 1 ) = n ) |
162 |
157 161
|
breqtrrd |
|- ( ( T. /\ n e. NN ) -> 1 <_ ( n x. 1 ) ) |
163 |
|
1red |
|- ( ( T. /\ n e. NN ) -> 1 e. RR ) |
164 |
|
nngt0 |
|- ( n e. NN -> 0 < n ) |
165 |
164
|
adantl |
|- ( ( T. /\ n e. NN ) -> 0 < n ) |
166 |
|
ledivmul |
|- ( ( 1 e. RR /\ 1 e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( ( 1 / n ) <_ 1 <-> 1 <_ ( n x. 1 ) ) ) |
167 |
163 163 159 165 166
|
syl112anc |
|- ( ( T. /\ n e. NN ) -> ( ( 1 / n ) <_ 1 <-> 1 <_ ( n x. 1 ) ) ) |
168 |
162 167
|
mpbird |
|- ( ( T. /\ n e. NN ) -> ( 1 / n ) <_ 1 ) |
169 |
|
elicc01 |
|- ( ( 1 / n ) e. ( 0 [,] 1 ) <-> ( ( 1 / n ) e. RR /\ 0 <_ ( 1 / n ) /\ ( 1 / n ) <_ 1 ) ) |
170 |
154 155 168 169
|
syl3anbrc |
|- ( ( T. /\ n e. NN ) -> ( 1 / n ) e. ( 0 [,] 1 ) ) |
171 |
|
iirev |
|- ( ( 1 / n ) e. ( 0 [,] 1 ) -> ( 1 - ( 1 / n ) ) e. ( 0 [,] 1 ) ) |
172 |
170 171
|
syl |
|- ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / n ) ) e. ( 0 [,] 1 ) ) |
173 |
172
|
fmpttd |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) : NN --> ( 0 [,] 1 ) ) |
174 |
|
1cnd |
|- ( T. -> 1 e. CC ) |
175 |
|
nnex |
|- NN e. _V |
176 |
175
|
mptex |
|- ( n e. NN |-> ( 1 - ( 1 / n ) ) ) e. _V |
177 |
176
|
a1i |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) e. _V ) |
178 |
90
|
recnd |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) e. CC ) |
179 |
83
|
oveq2d |
|- ( n = k -> ( 1 - ( 1 / n ) ) = ( 1 - ( 1 / k ) ) ) |
180 |
|
eqid |
|- ( n e. NN |-> ( 1 - ( 1 / n ) ) ) = ( n e. NN |-> ( 1 - ( 1 / n ) ) ) |
181 |
|
ovex |
|- ( 1 - ( 1 / k ) ) e. _V |
182 |
179 180 181
|
fvmpt |
|- ( k e. NN -> ( ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ` k ) = ( 1 - ( 1 / k ) ) ) |
183 |
86
|
oveq2d |
|- ( k e. NN -> ( 1 - ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) = ( 1 - ( 1 / k ) ) ) |
184 |
182 183
|
eqtr4d |
|- ( k e. NN -> ( ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ` k ) = ( 1 - ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) ) |
185 |
184
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ` k ) = ( 1 - ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) ) |
186 |
75 76 79 174 177 178 185
|
climsubc2 |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ~~> ( 1 - 0 ) ) |
187 |
|
1m0e1 |
|- ( 1 - 0 ) = 1 |
188 |
186 187
|
breqtrdi |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ~~> 1 ) |
189 |
|
1elunit |
|- 1 e. ( 0 [,] 1 ) |
190 |
189
|
a1i |
|- ( T. -> 1 e. ( 0 [,] 1 ) ) |
191 |
75 76 150 173 188 190
|
climcncf |
|- ( T. -> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) o. ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) ~~> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) ` 1 ) ) |
192 |
|
eqidd |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) = ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) |
193 |
|
eqidd |
|- ( T. -> ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) = ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) ) |
194 |
|
oveq1 |
|- ( x = ( 1 - ( 1 / n ) ) -> ( x ^ j ) = ( ( 1 - ( 1 / n ) ) ^ j ) ) |
195 |
194
|
oveq2d |
|- ( x = ( 1 - ( 1 / n ) ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
196 |
195
|
sumeq2sdv |
|- ( x = ( 1 - ( 1 / n ) ) -> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) = sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
197 |
172 192 193 196
|
fmptco |
|- ( T. -> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) o. ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) = ( n e. NN |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) ) |
198 |
|
0zd |
|- ( ( T. /\ n e. NN ) -> 0 e. ZZ ) |
199 |
9
|
adantll |
|- ( ( ( T. /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( k - 1 ) / 2 ) e. NN0 ) |
200 |
7 199 10
|
sylancr |
|- ( ( ( T. /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. RR ) |
201 |
200
|
recnd |
|- ( ( ( T. /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. CC ) |
202 |
201
|
adantllr |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. CC ) |
203 |
|
1re |
|- 1 e. RR |
204 |
|
resubcl |
|- ( ( 1 e. RR /\ ( 1 / n ) e. RR ) -> ( 1 - ( 1 / n ) ) e. RR ) |
205 |
203 154 204
|
sylancr |
|- ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / n ) ) e. RR ) |
206 |
205
|
ad2antrr |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( 1 - ( 1 / n ) ) e. RR ) |
207 |
|
simplr |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> k e. NN0 ) |
208 |
206 207
|
reexpcld |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( 1 - ( 1 / n ) ) ^ k ) e. RR ) |
209 |
208
|
recnd |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( 1 - ( 1 / n ) ) ^ k ) e. CC ) |
210 |
|
nn0cn |
|- ( k e. NN0 -> k e. CC ) |
211 |
210
|
ad2antlr |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> k e. CC ) |
212 |
12
|
adantll |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> k e. NN ) |
213 |
212
|
nnne0d |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> k =/= 0 ) |
214 |
202 209 211 213
|
div12d |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) = ( ( ( 1 - ( 1 / n ) ) ^ k ) x. ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) |
215 |
14
|
adantll |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. CC ) |
216 |
209 215
|
mulcomd |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( ( 1 - ( 1 / n ) ) ^ k ) x. ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) = ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
217 |
214 216
|
eqtrd |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) = ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
218 |
6 217
|
sylan2b |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ -. ( k = 0 \/ 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) = ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
219 |
218
|
ifeq2da |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) ) |
220 |
205
|
recnd |
|- ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / n ) ) e. CC ) |
221 |
|
expcl |
|- ( ( ( 1 - ( 1 / n ) ) e. CC /\ k e. NN0 ) -> ( ( 1 - ( 1 / n ) ) ^ k ) e. CC ) |
222 |
220 221
|
sylan |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( ( 1 - ( 1 / n ) ) ^ k ) e. CC ) |
223 |
222
|
mul02d |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( 0 x. ( ( 1 - ( 1 / n ) ) ^ k ) ) = 0 ) |
224 |
223
|
ifeq1d |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , ( 0 x. ( ( 1 - ( 1 / n ) ) ^ k ) ) , ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) ) |
225 |
219 224
|
eqtr4d |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = if ( ( k = 0 \/ 2 || k ) , ( 0 x. ( ( 1 - ( 1 / n ) ) ^ k ) ) , ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) ) |
226 |
|
ovif |
|- ( if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) = if ( ( k = 0 \/ 2 || k ) , ( 0 x. ( ( 1 - ( 1 / n ) ) ^ k ) ) , ( ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
227 |
225 226
|
eqtr4di |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = ( if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
228 |
|
simpr |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> k e. NN0 ) |
229 |
|
c0ex |
|- 0 e. _V |
230 |
|
ovex |
|- ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) e. _V |
231 |
229 230
|
ifex |
|- if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) e. _V |
232 |
|
eqid |
|- ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) = ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
233 |
232
|
fvmpt2 |
|- ( ( k e. NN0 /\ if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) e. _V ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
234 |
228 231 233
|
sylancl |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
235 |
|
ovex |
|- ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. _V |
236 |
229 235
|
ifex |
|- if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) e. _V |
237 |
141
|
fvmpt2 |
|- ( ( k e. NN0 /\ if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) e. _V ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) |
238 |
228 236 237
|
sylancl |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) |
239 |
238
|
oveq1d |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) = ( if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
240 |
227 234 239
|
3eqtr4d |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
241 |
240
|
ralrimiva |
|- ( ( T. /\ n e. NN ) -> A. k e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) ) |
242 |
|
nfv |
|- F/ j ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) |
243 |
|
nffvmpt1 |
|- F/_ k ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) |
244 |
|
nffvmpt1 |
|- F/_ k ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) |
245 |
|
nfcv |
|- F/_ k x. |
246 |
|
nfcv |
|- F/_ k ( ( 1 - ( 1 / n ) ) ^ j ) |
247 |
244 245 246
|
nfov |
|- F/_ k ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) |
248 |
243 247
|
nfeq |
|- F/ k ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) |
249 |
|
fveq2 |
|- ( k = j -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
250 |
|
fveq2 |
|- ( k = j -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
251 |
|
oveq2 |
|- ( k = j -> ( ( 1 - ( 1 / n ) ) ^ k ) = ( ( 1 - ( 1 / n ) ) ^ j ) ) |
252 |
250 251
|
oveq12d |
|- ( k = j -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
253 |
249 252
|
eqeq12d |
|- ( k = j -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) <-> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) ) |
254 |
242 248 253
|
cbvralw |
|- ( A. k e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` k ) x. ( ( 1 - ( 1 / n ) ) ^ k ) ) <-> A. j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
255 |
241 254
|
sylib |
|- ( ( T. /\ n e. NN ) -> A. j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
256 |
255
|
r19.21bi |
|- ( ( ( T. /\ n e. NN ) /\ j e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) |
257 |
|
0cnd |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( k = 0 \/ 2 || k ) ) -> 0 e. CC ) |
258 |
208 212
|
nndivred |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) e. RR ) |
259 |
258
|
recnd |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) e. CC ) |
260 |
202 259
|
mulcld |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) e. CC ) |
261 |
6 260
|
sylan2b |
|- ( ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) /\ -. ( k = 0 \/ 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) e. CC ) |
262 |
257 261
|
ifclda |
|- ( ( ( T. /\ n e. NN ) /\ k e. NN0 ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) e. CC ) |
263 |
262
|
fmpttd |
|- ( ( T. /\ n e. NN ) -> ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) : NN0 --> CC ) |
264 |
263
|
ffvelrnda |
|- ( ( ( T. /\ n e. NN ) /\ j e. NN0 ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) e. CC ) |
265 |
256 264
|
eqeltrrd |
|- ( ( ( T. /\ n e. NN ) /\ j e. NN0 ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) e. CC ) |
266 |
|
0nn0 |
|- 0 e. NN0 |
267 |
266
|
a1i |
|- ( ( T. /\ n e. NN ) -> 0 e. NN0 ) |
268 |
|
0p1e1 |
|- ( 0 + 1 ) = 1 |
269 |
|
seqeq1 |
|- ( ( 0 + 1 ) = 1 -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) = seq 1 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ) |
270 |
268 269
|
ax-mp |
|- seq ( 0 + 1 ) ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) = seq 1 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) |
271 |
|
1zzd |
|- ( ( T. /\ n e. NN ) -> 1 e. ZZ ) |
272 |
|
elnnuz |
|- ( j e. NN <-> j e. ( ZZ>= ` 1 ) ) |
273 |
|
nnne0 |
|- ( k e. NN -> k =/= 0 ) |
274 |
273
|
neneqd |
|- ( k e. NN -> -. k = 0 ) |
275 |
|
biorf |
|- ( -. k = 0 -> ( 2 || k <-> ( k = 0 \/ 2 || k ) ) ) |
276 |
274 275
|
syl |
|- ( k e. NN -> ( 2 || k <-> ( k = 0 \/ 2 || k ) ) ) |
277 |
276
|
bicomd |
|- ( k e. NN -> ( ( k = 0 \/ 2 || k ) <-> 2 || k ) ) |
278 |
277
|
ifbid |
|- ( k e. NN -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
279 |
91 231 233
|
sylancl |
|- ( k e. NN -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
280 |
229 230
|
ifex |
|- if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) e. _V |
281 |
|
eqid |
|- ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) = ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
282 |
281
|
fvmpt2 |
|- ( ( k e. NN /\ if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) e. _V ) -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
283 |
280 282
|
mpan2 |
|- ( k e. NN -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) |
284 |
278 279 283
|
3eqtr4d |
|- ( k e. NN -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) ) |
285 |
284
|
rgen |
|- A. k e. NN ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) |
286 |
285
|
a1i |
|- ( ( T. /\ n e. NN ) -> A. k e. NN ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) ) |
287 |
|
nfv |
|- F/ j ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) |
288 |
|
nffvmpt1 |
|- F/_ k ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) |
289 |
243 288
|
nfeq |
|- F/ k ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) |
290 |
|
fveq2 |
|- ( k = j -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
291 |
249 290
|
eqeq12d |
|- ( k = j -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) <-> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) ) |
292 |
287 289 291
|
cbvralw |
|- ( A. k e. NN ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` k ) <-> A. j e. NN ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
293 |
286 292
|
sylib |
|- ( ( T. /\ n e. NN ) -> A. j e. NN ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
294 |
293
|
r19.21bi |
|- ( ( ( T. /\ n e. NN ) /\ j e. NN ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
295 |
272 294
|
sylan2br |
|- ( ( ( T. /\ n e. NN ) /\ j e. ( ZZ>= ` 1 ) ) -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) = ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` j ) ) |
296 |
271 295
|
seqfeq |
|- ( ( T. /\ n e. NN ) -> seq 1 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) = seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ) |
297 |
154 163 168
|
abssubge0d |
|- ( ( T. /\ n e. NN ) -> ( abs ` ( 1 - ( 1 / n ) ) ) = ( 1 - ( 1 / n ) ) ) |
298 |
|
ltsubrp |
|- ( ( 1 e. RR /\ ( 1 / n ) e. RR+ ) -> ( 1 - ( 1 / n ) ) < 1 ) |
299 |
203 153 298
|
sylancr |
|- ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / n ) ) < 1 ) |
300 |
297 299
|
eqbrtrd |
|- ( ( T. /\ n e. NN ) -> ( abs ` ( 1 - ( 1 / n ) ) ) < 1 ) |
301 |
281
|
atantayl2 |
|- ( ( ( 1 - ( 1 / n ) ) e. CC /\ ( abs ` ( 1 - ( 1 / n ) ) ) < 1 ) -> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
302 |
220 300 301
|
syl2anc |
|- ( ( T. /\ n e. NN ) -> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
303 |
296 302
|
eqbrtrd |
|- ( ( T. /\ n e. NN ) -> seq 1 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
304 |
270 303
|
eqbrtrid |
|- ( ( T. /\ n e. NN ) -> seq ( 0 + 1 ) ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
305 |
2 267 264 304
|
clim2ser2 |
|- ( ( T. /\ n e. NN ) -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( ( arctan ` ( 1 - ( 1 / n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) ) ) |
306 |
|
0z |
|- 0 e. ZZ |
307 |
|
seq1 |
|- ( 0 e. ZZ -> ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` 0 ) ) |
308 |
306 307
|
ax-mp |
|- ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` 0 ) |
309 |
|
iftrue |
|- ( ( k = 0 \/ 2 || k ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = 0 ) |
310 |
309
|
orcs |
|- ( k = 0 -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) = 0 ) |
311 |
310 232 229
|
fvmpt |
|- ( 0 e. NN0 -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` 0 ) = 0 ) |
312 |
266 311
|
ax-mp |
|- ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ` 0 ) = 0 |
313 |
308 312
|
eqtri |
|- ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) = 0 |
314 |
313
|
oveq2i |
|- ( ( arctan ` ( 1 - ( 1 / n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) ) = ( ( arctan ` ( 1 - ( 1 / n ) ) ) + 0 ) |
315 |
|
atanrecl |
|- ( ( 1 - ( 1 / n ) ) e. RR -> ( arctan ` ( 1 - ( 1 / n ) ) ) e. RR ) |
316 |
205 315
|
syl |
|- ( ( T. /\ n e. NN ) -> ( arctan ` ( 1 - ( 1 / n ) ) ) e. RR ) |
317 |
316
|
recnd |
|- ( ( T. /\ n e. NN ) -> ( arctan ` ( 1 - ( 1 / n ) ) ) e. CC ) |
318 |
317
|
addid1d |
|- ( ( T. /\ n e. NN ) -> ( ( arctan ` ( 1 - ( 1 / n ) ) ) + 0 ) = ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
319 |
314 318
|
syl5eq |
|- ( ( T. /\ n e. NN ) -> ( ( arctan ` ( 1 - ( 1 / n ) ) ) + ( seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ` 0 ) ) = ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
320 |
305 319
|
breqtrd |
|- ( ( T. /\ n e. NN ) -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( ( 1 - ( 1 / n ) ) ^ k ) / k ) ) ) ) ) ~~> ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
321 |
2 198 256 265 320
|
isumclim |
|- ( ( T. /\ n e. NN ) -> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) = ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
322 |
321
|
mpteq2dva |
|- ( T. -> ( n e. NN |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( ( 1 - ( 1 / n ) ) ^ j ) ) ) = ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ) |
323 |
197 322
|
eqtrd |
|- ( T. -> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) o. ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) = ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ) |
324 |
|
oveq1 |
|- ( x = 1 -> ( x ^ j ) = ( 1 ^ j ) ) |
325 |
|
nn0z |
|- ( j e. NN0 -> j e. ZZ ) |
326 |
|
1exp |
|- ( j e. ZZ -> ( 1 ^ j ) = 1 ) |
327 |
325 326
|
syl |
|- ( j e. NN0 -> ( 1 ^ j ) = 1 ) |
328 |
324 327
|
sylan9eq |
|- ( ( x = 1 /\ j e. NN0 ) -> ( x ^ j ) = 1 ) |
329 |
328
|
oveq2d |
|- ( ( x = 1 /\ j e. NN0 ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) = ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. 1 ) ) |
330 |
18
|
mptru |
|- ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) : NN0 --> CC |
331 |
330
|
ffvelrni |
|- ( j e. NN0 -> ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) e. CC ) |
332 |
331
|
mulid1d |
|- ( j e. NN0 -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. 1 ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
333 |
332
|
adantl |
|- ( ( x = 1 /\ j e. NN0 ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. 1 ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
334 |
329 333
|
eqtrd |
|- ( ( x = 1 /\ j e. NN0 ) -> ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) = ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
335 |
334
|
sumeq2dv |
|- ( x = 1 -> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) = sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
336 |
|
sumex |
|- sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) e. _V |
337 |
335 149 336
|
fvmpt |
|- ( 1 e. ( 0 [,] 1 ) -> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) ` 1 ) = sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
338 |
189 337
|
mp1i |
|- ( T. -> ( ( x e. ( 0 [,] 1 ) |-> sum_ j e. NN0 ( ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) x. ( x ^ j ) ) ) ` 1 ) = sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
339 |
191 323 338
|
3brtr3d |
|- ( T. -> ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ~~> sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) ) |
340 |
|
eqid |
|- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) ) |
341 |
|
eqid |
|- { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } = { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |
342 |
340 341
|
atancn |
|- ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) e. ( { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } -cn-> CC ) |
343 |
342
|
a1i |
|- ( T. -> ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) e. ( { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } -cn-> CC ) ) |
344 |
|
unitssre |
|- ( 0 [,] 1 ) C_ RR |
345 |
340 341
|
ressatans |
|- RR C_ { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |
346 |
344 345
|
sstri |
|- ( 0 [,] 1 ) C_ { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |
347 |
|
fss |
|- ( ( ( n e. NN |-> ( 1 - ( 1 / n ) ) ) : NN --> ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) : NN --> { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) |
348 |
173 346 347
|
sylancl |
|- ( T. -> ( n e. NN |-> ( 1 - ( 1 / n ) ) ) : NN --> { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) |
349 |
345 203
|
sselii |
|- 1 e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |
350 |
349
|
a1i |
|- ( T. -> 1 e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) |
351 |
75 76 343 348 188 350
|
climcncf |
|- ( T. -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) o. ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) ~~> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` 1 ) ) |
352 |
346 172
|
sselid |
|- ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / n ) ) e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) |
353 |
|
cncff |
|- ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) e. ( { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } -cn-> CC ) -> ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) : { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } --> CC ) |
354 |
342 353
|
mp1i |
|- ( T. -> ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) : { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } --> CC ) |
355 |
354
|
feqmptd |
|- ( T. -> ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) = ( k e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |-> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` k ) ) ) |
356 |
|
fvres |
|- ( k e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` k ) = ( arctan ` k ) ) |
357 |
356
|
mpteq2ia |
|- ( k e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |-> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` k ) ) = ( k e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |-> ( arctan ` k ) ) |
358 |
355 357
|
eqtrdi |
|- ( T. -> ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) = ( k e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } |-> ( arctan ` k ) ) ) |
359 |
|
fveq2 |
|- ( k = ( 1 - ( 1 / n ) ) -> ( arctan ` k ) = ( arctan ` ( 1 - ( 1 / n ) ) ) ) |
360 |
352 192 358 359
|
fmptco |
|- ( T. -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) o. ( n e. NN |-> ( 1 - ( 1 / n ) ) ) ) = ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ) |
361 |
|
fvres |
|- ( 1 e. { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` 1 ) = ( arctan ` 1 ) ) |
362 |
349 361
|
mp1i |
|- ( T. -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` 1 ) = ( arctan ` 1 ) ) |
363 |
|
atan1 |
|- ( arctan ` 1 ) = ( _pi / 4 ) |
364 |
362 363
|
eqtrdi |
|- ( T. -> ( ( arctan |` { x e. CC | ( 1 + ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) } ) ` 1 ) = ( _pi / 4 ) ) |
365 |
351 360 364
|
3brtr3d |
|- ( T. -> ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ~~> ( _pi / 4 ) ) |
366 |
|
climuni |
|- ( ( ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ~~> sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) /\ ( n e. NN |-> ( arctan ` ( 1 - ( 1 / n ) ) ) ) ~~> ( _pi / 4 ) ) -> sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) = ( _pi / 4 ) ) |
367 |
339 365 366
|
syl2anc |
|- ( T. -> sum_ j e. NN0 ( ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` j ) = ( _pi / 4 ) ) |
368 |
148 367
|
breqtrd |
|- ( T. -> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( _pi / 4 ) ) |
369 |
368
|
mptru |
|- seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( _pi / 4 ) |
370 |
|
ovex |
|- ( _pi / 4 ) e. _V |
371 |
1 141 370
|
leibpilem2 |
|- ( seq 0 ( + , F ) ~~> ( _pi / 4 ) <-> seq 0 ( + , ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> ( _pi / 4 ) ) |
372 |
369 371
|
mpbir |
|- seq 0 ( + , F ) ~~> ( _pi / 4 ) |