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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
Assertion log2cnv seq 0 ( + , 𝐹 ) ⇝ ( log ‘ 2 )

Proof

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