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 )