Metamath Proof Explorer


Theorem leibpi

Description: The Leibniz formula for _pi . This proof depends on three main facts: (1) the series F is convergent, because it is an alternating series ( iseralt ). (2) Using leibpilem2 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan ( atantayl2 ). (3) Although we cannot directly plug x = 1 into atantayl2 , Abel's theorem ( abelth2 ) says that the limit along any sequence converging to 1 , such as 1 - 1 / n , of the power series converges to the power series extended to 1 , and then since arctan is continuous at 1 ( atancn ) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypothesis leibpi.1
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
Assertion leibpi
|- seq 0 ( + , F ) ~~> ( _pi / 4 )

Proof

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 )