Metamath Proof Explorer

Theorem log2cnv

Description: Using the Taylor series for arctan ( _i / 3 ) , produce a rapidly convergent series for log 2 . (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypothesis log2cnv.1 
|- F = ( n e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
Assertion log2cnv 
|- seq 0 ( + , F ) ~~> ( log ` 2 )

Proof

Step Hyp Ref Expression
1 log2cnv.1 
 |-  F = ( n e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 0zd 
 |-  ( T. -> 0 e. ZZ )
4 2cn 
 |-  2 e. CC
5 ax-icn 
 |-  _i e. CC
6 ine0 
 |-  _i =/= 0
7 4 5 6 divcli 
 |-  ( 2 / _i ) e. CC
8 7 a1i 
 |-  ( T. -> ( 2 / _i ) e. CC )
9 3cn 
 |-  3 e. CC
10 3ne0 
 |-  3 =/= 0
11 5 9 10 divcli 
 |-  ( _i / 3 ) e. CC
12 absdiv 
 |-  ( ( _i e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( abs ` ( _i / 3 ) ) = ( ( abs ` _i ) / ( abs ` 3 ) ) )
13 5 9 10 12 mp3an 
 |-  ( abs ` ( _i / 3 ) ) = ( ( abs ` _i ) / ( abs ` 3 ) )
14 absi 
 |-  ( abs ` _i ) = 1
15 3re 
 |-  3 e. RR
16 0re 
 |-  0 e. RR
17 3pos 
 |-  0 < 3
18 16 15 17 ltleii 
 |-  0 <_ 3
19 absid 
 |-  ( ( 3 e. RR /\ 0 <_ 3 ) -> ( abs ` 3 ) = 3 )
20 15 18 19 mp2an 
 |-  ( abs ` 3 ) = 3
21 14 20 oveq12i 
 |-  ( ( abs ` _i ) / ( abs ` 3 ) ) = ( 1 / 3 )
22 13 21 eqtri 
 |-  ( abs ` ( _i / 3 ) ) = ( 1 / 3 )
23 1lt3 
 |-  1 < 3
24 recgt1 
 |-  ( ( 3 e. RR /\ 0 < 3 ) -> ( 1 < 3 <-> ( 1 / 3 ) < 1 ) )
25 15 17 24 mp2an 
 |-  ( 1 < 3 <-> ( 1 / 3 ) < 1 )
26 23 25 mpbi 
 |-  ( 1 / 3 ) < 1
27 22 26 eqbrtri 
 |-  ( abs ` ( _i / 3 ) ) < 1
28 eqid 
 |-  ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) )
29 28 atantayl3 
 |-  ( ( ( _i / 3 ) e. CC /\ ( abs ` ( _i / 3 ) ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ~~> ( arctan ` ( _i / 3 ) ) )
30 11 27 29 mp2an 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ~~> ( arctan ` ( _i / 3 ) )
31 30 a1i 
 |-  ( T. -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ~~> ( arctan ` ( _i / 3 ) ) )
32 oveq2 
 |-  ( n = k -> ( -u 1 ^ n ) = ( -u 1 ^ k ) )
33 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
34 33 oveq1d 
 |-  ( n = k -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. k ) + 1 ) )
35 34 oveq2d 
 |-  ( n = k -> ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) = ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) )
36 35 34 oveq12d 
 |-  ( n = k -> ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) = ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) )
37 32 36 oveq12d 
 |-  ( n = k -> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) = ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) )
38 ovex 
 |-  ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) e. _V
39 37 28 38 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) = ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) )
40 5 a1i 
 |-  ( k e. NN0 -> _i e. CC )
41 9 a1i 
 |-  ( k e. NN0 -> 3 e. CC )
42 10 a1i 
 |-  ( k e. NN0 -> 3 =/= 0 )
43 2nn0 
 |-  2 e. NN0
44 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
45 43 44 mpan 
 |-  ( k e. NN0 -> ( 2 x. k ) e. NN0 )
46 peano2nn0 
 |-  ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN0 )
47 45 46 syl 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN0 )
48 40 41 42 47 expdivd 
 |-  ( k e. NN0 -> ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) = ( ( _i ^ ( ( 2 x. k ) + 1 ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) )
49 48 oveq2d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( -u 1 ^ k ) x. ( ( _i ^ ( ( 2 x. k ) + 1 ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) ) )
50 neg1cn 
 |-  -u 1 e. CC
51 expcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC )
52 50 51 mpan 
 |-  ( k e. NN0 -> ( -u 1 ^ k ) e. CC )
53 expcl 
 |-  ( ( _i e. CC /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( _i ^ ( ( 2 x. k ) + 1 ) ) e. CC )
54 5 47 53 sylancr 
 |-  ( k e. NN0 -> ( _i ^ ( ( 2 x. k ) + 1 ) ) e. CC )
55 3nn 
 |-  3 e. NN
56 nnexpcl 
 |-  ( ( 3 e. NN /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) e. NN )
57 55 47 56 sylancr 
 |-  ( k e. NN0 -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) e. NN )
58 57 nncnd 
 |-  ( k e. NN0 -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) e. CC )
59 57 nnne0d 
 |-  ( k e. NN0 -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) =/= 0 )
60 52 54 58 59 divassd 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( _i ^ ( ( 2 x. k ) + 1 ) ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( -u 1 ^ k ) x. ( ( _i ^ ( ( 2 x. k ) + 1 ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) ) )
61 expp1 
 |-  ( ( _i e. CC /\ ( 2 x. k ) e. NN0 ) -> ( _i ^ ( ( 2 x. k ) + 1 ) ) = ( ( _i ^ ( 2 x. k ) ) x. _i ) )
62 5 45 61 sylancr 
 |-  ( k e. NN0 -> ( _i ^ ( ( 2 x. k ) + 1 ) ) = ( ( _i ^ ( 2 x. k ) ) x. _i ) )
63 expmul 
 |-  ( ( _i e. CC /\ 2 e. NN0 /\ k e. NN0 ) -> ( _i ^ ( 2 x. k ) ) = ( ( _i ^ 2 ) ^ k ) )
64 5 43 63 mp3an12 
 |-  ( k e. NN0 -> ( _i ^ ( 2 x. k ) ) = ( ( _i ^ 2 ) ^ k ) )
65 i2 
 |-  ( _i ^ 2 ) = -u 1
66 65 oveq1i 
 |-  ( ( _i ^ 2 ) ^ k ) = ( -u 1 ^ k )
67 64 66 eqtrdi 
 |-  ( k e. NN0 -> ( _i ^ ( 2 x. k ) ) = ( -u 1 ^ k ) )
68 67 oveq1d 
 |-  ( k e. NN0 -> ( ( _i ^ ( 2 x. k ) ) x. _i ) = ( ( -u 1 ^ k ) x. _i ) )
69 62 68 eqtrd 
 |-  ( k e. NN0 -> ( _i ^ ( ( 2 x. k ) + 1 ) ) = ( ( -u 1 ^ k ) x. _i ) )
70 69 oveq2d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( _i ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( -u 1 ^ k ) x. ( ( -u 1 ^ k ) x. _i ) ) )
71 52 52 40 mulassd 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( -u 1 ^ k ) ) x. _i ) = ( ( -u 1 ^ k ) x. ( ( -u 1 ^ k ) x. _i ) ) )
72 50 a1i 
 |-  ( k e. NN0 -> -u 1 e. CC )
73 id 
 |-  ( k e. NN0 -> k e. NN0 )
74 72 73 73 expaddd 
 |-  ( k e. NN0 -> ( -u 1 ^ ( k + k ) ) = ( ( -u 1 ^ k ) x. ( -u 1 ^ k ) ) )
75 expmul 
 |-  ( ( -u 1 e. CC /\ 2 e. NN0 /\ k e. NN0 ) -> ( -u 1 ^ ( 2 x. k ) ) = ( ( -u 1 ^ 2 ) ^ k ) )
76 50 43 75 mp3an12 
 |-  ( k e. NN0 -> ( -u 1 ^ ( 2 x. k ) ) = ( ( -u 1 ^ 2 ) ^ k ) )
77 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
78 77 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ k ) = ( 1 ^ k )
79 76 78 eqtrdi 
 |-  ( k e. NN0 -> ( -u 1 ^ ( 2 x. k ) ) = ( 1 ^ k ) )
80 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
81 80 2timesd 
 |-  ( k e. NN0 -> ( 2 x. k ) = ( k + k ) )
82 81 oveq2d 
 |-  ( k e. NN0 -> ( -u 1 ^ ( 2 x. k ) ) = ( -u 1 ^ ( k + k ) ) )
83 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
84 1exp 
 |-  ( k e. ZZ -> ( 1 ^ k ) = 1 )
85 83 84 syl 
 |-  ( k e. NN0 -> ( 1 ^ k ) = 1 )
86 79 82 85 3eqtr3d 
 |-  ( k e. NN0 -> ( -u 1 ^ ( k + k ) ) = 1 )
87 74 86 eqtr3d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( -u 1 ^ k ) ) = 1 )
88 87 oveq1d 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( -u 1 ^ k ) ) x. _i ) = ( 1 x. _i ) )
89 5 mulid2i 
 |-  ( 1 x. _i ) = _i
90 88 89 eqtrdi 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( -u 1 ^ k ) ) x. _i ) = _i )
91 70 71 90 3eqtr2d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( _i ^ ( ( 2 x. k ) + 1 ) ) ) = _i )
92 91 oveq1d 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( _i ^ ( ( 2 x. k ) + 1 ) ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) )
93 49 60 92 3eqtr2d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) )
94 93 oveq1d 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) / ( ( 2 x. k ) + 1 ) ) = ( ( _i / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) / ( ( 2 x. k ) + 1 ) ) )
95 expcl 
 |-  ( ( ( _i / 3 ) e. CC /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) e. CC )
96 11 47 95 sylancr 
 |-  ( k e. NN0 -> ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) e. CC )
97 nn0p1nn 
 |-  ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN )
98 45 97 syl 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN )
99 98 nncnd 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. CC )
100 98 nnne0d 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) =/= 0 )
101 52 96 99 100 divassd 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) / ( ( 2 x. k ) + 1 ) ) = ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) )
102 40 58 99 59 100 divdiv1d 
 |-  ( k e. NN0 -> ( ( _i / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) / ( ( 2 x. k ) + 1 ) ) = ( _i / ( ( 3 ^ ( ( 2 x. k ) + 1 ) ) x. ( ( 2 x. k ) + 1 ) ) ) )
103 94 101 102 3eqtr3d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( ( 3 ^ ( ( 2 x. k ) + 1 ) ) x. ( ( 2 x. k ) + 1 ) ) ) )
104 58 99 mulcomd 
 |-  ( k e. NN0 -> ( ( 3 ^ ( ( 2 x. k ) + 1 ) ) x. ( ( 2 x. k ) + 1 ) ) = ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) )
105 104 oveq2d 
 |-  ( k e. NN0 -> ( _i / ( ( 3 ^ ( ( 2 x. k ) + 1 ) ) x. ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) ) )
106 39 103 105 3eqtrd 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) = ( _i / ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) ) )
107 98 57 nnmulcld 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) e. NN )
108 107 nncnd 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) e. CC )
109 107 nnne0d 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) =/= 0 )
110 40 108 109 divcld 
 |-  ( k e. NN0 -> ( _i / ( ( ( 2 x. k ) + 1 ) x. ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) ) e. CC )
111 106 110 eqeltrd 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) e. CC )
112 111 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) e. CC )
113 34 oveq2d 
 |-  ( n = k -> ( 3 x. ( ( 2 x. n ) + 1 ) ) = ( 3 x. ( ( 2 x. k ) + 1 ) ) )
114 oveq2 
 |-  ( n = k -> ( 9 ^ n ) = ( 9 ^ k ) )
115 113 114 oveq12d 
 |-  ( n = k -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) = ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) )
116 115 oveq2d 
 |-  ( n = k -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
117 ovex 
 |-  ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) e. _V
118 116 1 117 fvmpt 
 |-  ( k e. NN0 -> ( F ` k ) = ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
119 expp1 
 |-  ( ( 3 e. CC /\ ( 2 x. k ) e. NN0 ) -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) = ( ( 3 ^ ( 2 x. k ) ) x. 3 ) )
120 9 45 119 sylancr 
 |-  ( k e. NN0 -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) = ( ( 3 ^ ( 2 x. k ) ) x. 3 ) )
121 expmul 
 |-  ( ( 3 e. CC /\ 2 e. NN0 /\ k e. NN0 ) -> ( 3 ^ ( 2 x. k ) ) = ( ( 3 ^ 2 ) ^ k ) )
122 9 43 121 mp3an12 
 |-  ( k e. NN0 -> ( 3 ^ ( 2 x. k ) ) = ( ( 3 ^ 2 ) ^ k ) )
123 sq3 
 |-  ( 3 ^ 2 ) = 9
124 123 oveq1i 
 |-  ( ( 3 ^ 2 ) ^ k ) = ( 9 ^ k )
125 122 124 eqtrdi 
 |-  ( k e. NN0 -> ( 3 ^ ( 2 x. k ) ) = ( 9 ^ k ) )
126 125 oveq1d 
 |-  ( k e. NN0 -> ( ( 3 ^ ( 2 x. k ) ) x. 3 ) = ( ( 9 ^ k ) x. 3 ) )
127 9nn 
 |-  9 e. NN
128 nnexpcl 
 |-  ( ( 9 e. NN /\ k e. NN0 ) -> ( 9 ^ k ) e. NN )
129 127 128 mpan 
 |-  ( k e. NN0 -> ( 9 ^ k ) e. NN )
130 129 nncnd 
 |-  ( k e. NN0 -> ( 9 ^ k ) e. CC )
131 mulcom 
 |-  ( ( ( 9 ^ k ) e. CC /\ 3 e. CC ) -> ( ( 9 ^ k ) x. 3 ) = ( 3 x. ( 9 ^ k ) ) )
132 130 9 131 sylancl 
 |-  ( k e. NN0 -> ( ( 9 ^ k ) x. 3 ) = ( 3 x. ( 9 ^ k ) ) )
133 120 126 132 3eqtrd 
 |-  ( k e. NN0 -> ( 3 ^ ( ( 2 x. k ) + 1 ) ) = ( 3 x. ( 9 ^ k ) ) )
134 91 133 oveq12d 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( _i ^ ( ( 2 x. k ) + 1 ) ) ) / ( 3 ^ ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( 3 x. ( 9 ^ k ) ) ) )
135 49 60 134 3eqtr2d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( 3 x. ( 9 ^ k ) ) ) )
136 135 oveq1d 
 |-  ( k e. NN0 -> ( ( ( -u 1 ^ k ) x. ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) ) / ( ( 2 x. k ) + 1 ) ) = ( ( _i / ( 3 x. ( 9 ^ k ) ) ) / ( ( 2 x. k ) + 1 ) ) )
137 nnmulcl 
 |-  ( ( 3 e. NN /\ ( 9 ^ k ) e. NN ) -> ( 3 x. ( 9 ^ k ) ) e. NN )
138 55 129 137 sylancr 
 |-  ( k e. NN0 -> ( 3 x. ( 9 ^ k ) ) e. NN )
139 138 nncnd 
 |-  ( k e. NN0 -> ( 3 x. ( 9 ^ k ) ) e. CC )
140 138 nnne0d 
 |-  ( k e. NN0 -> ( 3 x. ( 9 ^ k ) ) =/= 0 )
141 40 139 99 140 100 divdiv1d 
 |-  ( k e. NN0 -> ( ( _i / ( 3 x. ( 9 ^ k ) ) ) / ( ( 2 x. k ) + 1 ) ) = ( _i / ( ( 3 x. ( 9 ^ k ) ) x. ( ( 2 x. k ) + 1 ) ) ) )
142 136 101 141 3eqtr3d 
 |-  ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. k ) + 1 ) ) / ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( ( 3 x. ( 9 ^ k ) ) x. ( ( 2 x. k ) + 1 ) ) ) )
143 41 130 99 mul32d 
 |-  ( k e. NN0 -> ( ( 3 x. ( 9 ^ k ) ) x. ( ( 2 x. k ) + 1 ) ) = ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) )
144 143 oveq2d 
 |-  ( k e. NN0 -> ( _i / ( ( 3 x. ( 9 ^ k ) ) x. ( ( 2 x. k ) + 1 ) ) ) = ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
145 39 142 144 3eqtrd 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) = ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
146 145 oveq2d 
 |-  ( k e. NN0 -> ( ( 2 / _i ) x. ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) ) = ( ( 2 / _i ) x. ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) )
147 nnmulcl 
 |-  ( ( 3 e. NN /\ ( ( 2 x. k ) + 1 ) e. NN ) -> ( 3 x. ( ( 2 x. k ) + 1 ) ) e. NN )
148 55 98 147 sylancr 
 |-  ( k e. NN0 -> ( 3 x. ( ( 2 x. k ) + 1 ) ) e. NN )
149 148 129 nnmulcld 
 |-  ( k e. NN0 -> ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) e. NN )
150 149 nncnd 
 |-  ( k e. NN0 -> ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) e. CC )
151 149 nnne0d 
 |-  ( k e. NN0 -> ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) =/= 0 )
152 40 150 151 divcld 
 |-  ( k e. NN0 -> ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) e. CC )
153 mulcom 
 |-  ( ( ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) e. CC /\ ( 2 / _i ) e. CC ) -> ( ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) x. ( 2 / _i ) ) = ( ( 2 / _i ) x. ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) )
154 152 7 153 sylancl 
 |-  ( k e. NN0 -> ( ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) x. ( 2 / _i ) ) = ( ( 2 / _i ) x. ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) )
155 4 a1i 
 |-  ( k e. NN0 -> 2 e. CC )
156 6 a1i 
 |-  ( k e. NN0 -> _i =/= 0 )
157 155 40 150 156 151 dmdcand 
 |-  ( k e. NN0 -> ( ( _i / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) x. ( 2 / _i ) ) = ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
158 146 154 157 3eqtr2d 
 |-  ( k e. NN0 -> ( ( 2 / _i ) x. ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) ) = ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
159 118 158 eqtr4d 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( 2 / _i ) x. ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) ) )
160 159 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( F ` k ) = ( ( 2 / _i ) x. ( ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( ( _i / 3 ) ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ` k ) ) )
161 2 3 8 31 112 160 isermulc2 
 |-  ( T. -> seq 0 ( + , F ) ~~> ( ( 2 / _i ) x. ( arctan ` ( _i / 3 ) ) ) )
162 161 mptru 
 |-  seq 0 ( + , F ) ~~> ( ( 2 / _i ) x. ( arctan ` ( _i / 3 ) ) )
163 bndatandm 
 |-  ( ( ( _i / 3 ) e. CC /\ ( abs ` ( _i / 3 ) ) < 1 ) -> ( _i / 3 ) e. dom arctan )
164 11 27 163 mp2an 
 |-  ( _i / 3 ) e. dom arctan
165 atanval 
 |-  ( ( _i / 3 ) e. dom arctan -> ( arctan ` ( _i / 3 ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) - ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) ) ) )
166 164 165 ax-mp 
 |-  ( arctan ` ( _i / 3 ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) - ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) ) )
167 df-4 
 |-  4 = ( 3 + 1 )
168 167 oveq1i 
 |-  ( 4 / 3 ) = ( ( 3 + 1 ) / 3 )
169 ax-1cn 
 |-  1 e. CC
170 9 169 9 10 divdiri 
 |-  ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
171 9 10 dividi 
 |-  ( 3 / 3 ) = 1
172 171 oveq1i 
 |-  ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
173 168 170 172 3eqtri 
 |-  ( 4 / 3 ) = ( 1 + ( 1 / 3 ) )
174 169 9 10 divcli 
 |-  ( 1 / 3 ) e. CC
175 169 174 subnegi 
 |-  ( 1 - -u ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
176 divneg 
 |-  ( ( 1 e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> -u ( 1 / 3 ) = ( -u 1 / 3 ) )
177 169 9 10 176 mp3an 
 |-  -u ( 1 / 3 ) = ( -u 1 / 3 )
178 ixi 
 |-  ( _i x. _i ) = -u 1
179 178 oveq1i 
 |-  ( ( _i x. _i ) / 3 ) = ( -u 1 / 3 )
180 5 5 9 10 divassi 
 |-  ( ( _i x. _i ) / 3 ) = ( _i x. ( _i / 3 ) )
181 177 179 180 3eqtr2i 
 |-  -u ( 1 / 3 ) = ( _i x. ( _i / 3 ) )
182 181 oveq2i 
 |-  ( 1 - -u ( 1 / 3 ) ) = ( 1 - ( _i x. ( _i / 3 ) ) )
183 173 175 182 3eqtr2ri 
 |-  ( 1 - ( _i x. ( _i / 3 ) ) ) = ( 4 / 3 )
184 183 fveq2i 
 |-  ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) = ( log ` ( 4 / 3 ) )
185 9 10 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
186 divsubdir 
 |-  ( ( 3 e. CC /\ 1 e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) ) )
187 9 169 185 186 mp3an 
 |-  ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) )
188 3m1e2 
 |-  ( 3 - 1 ) = 2
189 188 oveq1i 
 |-  ( ( 3 - 1 ) / 3 ) = ( 2 / 3 )
190 171 oveq1i 
 |-  ( ( 3 / 3 ) - ( 1 / 3 ) ) = ( 1 - ( 1 / 3 ) )
191 187 189 190 3eqtr3i 
 |-  ( 2 / 3 ) = ( 1 - ( 1 / 3 ) )
192 169 174 negsubi 
 |-  ( 1 + -u ( 1 / 3 ) ) = ( 1 - ( 1 / 3 ) )
193 181 oveq2i 
 |-  ( 1 + -u ( 1 / 3 ) ) = ( 1 + ( _i x. ( _i / 3 ) ) )
194 191 192 193 3eqtr2ri 
 |-  ( 1 + ( _i x. ( _i / 3 ) ) ) = ( 2 / 3 )
195 194 fveq2i 
 |-  ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) = ( log ` ( 2 / 3 ) )
196 184 195 oveq12i 
 |-  ( ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) - ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) ) = ( ( log ` ( 4 / 3 ) ) - ( log ` ( 2 / 3 ) ) )
197 4re 
 |-  4 e. RR
198 4pos 
 |-  0 < 4
199 197 198 elrpii 
 |-  4 e. RR+
200 3rp 
 |-  3 e. RR+
201 rpdivcl 
 |-  ( ( 4 e. RR+ /\ 3 e. RR+ ) -> ( 4 / 3 ) e. RR+ )
202 199 200 201 mp2an 
 |-  ( 4 / 3 ) e. RR+
203 2rp 
 |-  2 e. RR+
204 rpdivcl 
 |-  ( ( 2 e. RR+ /\ 3 e. RR+ ) -> ( 2 / 3 ) e. RR+ )
205 203 200 204 mp2an 
 |-  ( 2 / 3 ) e. RR+
206 relogdiv 
 |-  ( ( ( 4 / 3 ) e. RR+ /\ ( 2 / 3 ) e. RR+ ) -> ( log ` ( ( 4 / 3 ) / ( 2 / 3 ) ) ) = ( ( log ` ( 4 / 3 ) ) - ( log ` ( 2 / 3 ) ) ) )
207 202 205 206 mp2an 
 |-  ( log ` ( ( 4 / 3 ) / ( 2 / 3 ) ) ) = ( ( log ` ( 4 / 3 ) ) - ( log ` ( 2 / 3 ) ) )
208 4cn 
 |-  4 e. CC
209 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
210 divcan7 
 |-  ( ( 4 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 4 / 3 ) / ( 2 / 3 ) ) = ( 4 / 2 ) )
211 208 209 185 210 mp3an 
 |-  ( ( 4 / 3 ) / ( 2 / 3 ) ) = ( 4 / 2 )
212 4d2e2 
 |-  ( 4 / 2 ) = 2
213 211 212 eqtri 
 |-  ( ( 4 / 3 ) / ( 2 / 3 ) ) = 2
214 213 fveq2i 
 |-  ( log ` ( ( 4 / 3 ) / ( 2 / 3 ) ) ) = ( log ` 2 )
215 196 207 214 3eqtr2i 
 |-  ( ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) - ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) ) = ( log ` 2 )
216 215 oveq2i 
 |-  ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( _i / 3 ) ) ) ) - ( log ` ( 1 + ( _i x. ( _i / 3 ) ) ) ) ) ) = ( ( _i / 2 ) x. ( log ` 2 ) )
217 166 216 eqtri 
 |-  ( arctan ` ( _i / 3 ) ) = ( ( _i / 2 ) x. ( log ` 2 ) )
218 217 oveq2i 
 |-  ( ( 2 / _i ) x. ( arctan ` ( _i / 3 ) ) ) = ( ( 2 / _i ) x. ( ( _i / 2 ) x. ( log ` 2 ) ) )
219 2ne0 
 |-  2 =/= 0
220 5 4 219 divcli 
 |-  ( _i / 2 ) e. CC
221 logcl 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( log ` 2 ) e. CC )
222 4 219 221 mp2an 
 |-  ( log ` 2 ) e. CC
223 7 220 222 mulassi 
 |-  ( ( ( 2 / _i ) x. ( _i / 2 ) ) x. ( log ` 2 ) ) = ( ( 2 / _i ) x. ( ( _i / 2 ) x. ( log ` 2 ) ) )
224 218 223 eqtr4i 
 |-  ( ( 2 / _i ) x. ( arctan ` ( _i / 3 ) ) ) = ( ( ( 2 / _i ) x. ( _i / 2 ) ) x. ( log ` 2 ) )
225 divcan6 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( 2 / _i ) x. ( _i / 2 ) ) = 1 )
226 4 219 5 6 225 mp4an 
 |-  ( ( 2 / _i ) x. ( _i / 2 ) ) = 1
227 226 oveq1i 
 |-  ( ( ( 2 / _i ) x. ( _i / 2 ) ) x. ( log ` 2 ) ) = ( 1 x. ( log ` 2 ) )
228 222 mulid2i 
 |-  ( 1 x. ( log ` 2 ) ) = ( log ` 2 )
229 224 227 228 3eqtri 
 |-  ( ( 2 / _i ) x. ( arctan ` ( _i / 3 ) ) ) = ( log ` 2 )
230 162 229 breqtri 
 |-  seq 0 ( + , F ) ~~> ( log ` 2 )