Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2cnv Structured version   Visualization version   GIF version

Theorem log2cnv 25534
 Description: Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
log2cnv.1 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
Assertion
Ref Expression
log2cnv seq0( + , 𝐹) ⇝ (log‘2)

Proof of Theorem log2cnv
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nn0uz 12272 . . . 4 0 = (ℤ‘0)
2 0zd 11985 . . . 4 (⊤ → 0 ∈ ℤ)
3 2cn 11704 . . . . . 6 2 ∈ ℂ
4 ax-icn 10589 . . . . . 6 i ∈ ℂ
5 ine0 11068 . . . . . 6 i ≠ 0
63, 4, 5divcli 11375 . . . . 5 (2 / i) ∈ ℂ
76a1i 11 . . . 4 (⊤ → (2 / i) ∈ ℂ)
8 3cn 11710 . . . . . . 7 3 ∈ ℂ
9 3ne0 11735 . . . . . . 7 3 ≠ 0
104, 8, 9divcli 11375 . . . . . 6 (i / 3) ∈ ℂ
11 absdiv 14651 . . . . . . . . 9 ((i ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (abs‘(i / 3)) = ((abs‘i) / (abs‘3)))
124, 8, 9, 11mp3an 1458 . . . . . . . 8 (abs‘(i / 3)) = ((abs‘i) / (abs‘3))
13 absi 14642 . . . . . . . . 9 (abs‘i) = 1
14 3re 11709 . . . . . . . . . 10 3 ∈ ℝ
15 0re 10636 . . . . . . . . . . 11 0 ∈ ℝ
16 3pos 11734 . . . . . . . . . . 11 0 < 3
1715, 14, 16ltleii 10756 . . . . . . . . . 10 0 ≤ 3
18 absid 14652 . . . . . . . . . 10 ((3 ∈ ℝ ∧ 0 ≤ 3) → (abs‘3) = 3)
1914, 17, 18mp2an 691 . . . . . . . . 9 (abs‘3) = 3
2013, 19oveq12i 7151 . . . . . . . 8 ((abs‘i) / (abs‘3)) = (1 / 3)
2112, 20eqtri 2824 . . . . . . 7 (abs‘(i / 3)) = (1 / 3)
22 1lt3 11802 . . . . . . . 8 1 < 3
23 recgt1 11529 . . . . . . . . 9 ((3 ∈ ℝ ∧ 0 < 3) → (1 < 3 ↔ (1 / 3) < 1))
2414, 16, 23mp2an 691 . . . . . . . 8 (1 < 3 ↔ (1 / 3) < 1)
2522, 24mpbi 233 . . . . . . 7 (1 / 3) < 1
2621, 25eqbrtri 5054 . . . . . 6 (abs‘(i / 3)) < 1
27 eqid 2801 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))
2827atantayl3 25529 . . . . . 6 (((i / 3) ∈ ℂ ∧ (abs‘(i / 3)) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝ (arctan‘(i / 3)))
2910, 26, 28mp2an 691 . . . . 5 seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝ (arctan‘(i / 3))
3029a1i 11 . . . 4 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝ (arctan‘(i / 3)))
31 oveq2 7147 . . . . . . . . 9 (𝑛 = 𝑘 → (-1↑𝑛) = (-1↑𝑘))
32 oveq2 7147 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
3332oveq1d 7154 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
3433oveq2d 7155 . . . . . . . . . 10 (𝑛 = 𝑘 → ((i / 3)↑((2 · 𝑛) + 1)) = ((i / 3)↑((2 · 𝑘) + 1)))
3534, 33oveq12d 7157 . . . . . . . . 9 (𝑛 = 𝑘 → (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)) = (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
3631, 35oveq12d 7157 . . . . . . . 8 (𝑛 = 𝑘 → ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) = ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
37 ovex 7172 . . . . . . . 8 ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ V
3836, 27, 37fvmpt 6749 . . . . . . 7 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
394a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → i ∈ ℂ)
408a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → 3 ∈ ℂ)
419a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → 3 ≠ 0)
42 2nn0 11906 . . . . . . . . . . . . . 14 2 ∈ ℕ0
43 nn0mulcl 11925 . . . . . . . . . . . . . 14 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
4442, 43mpan 689 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℕ0)
45 peano2nn0 11929 . . . . . . . . . . . . 13 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ0)
4644, 45syl 17 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ0)
4739, 40, 41, 46expdivd 13524 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((i / 3)↑((2 · 𝑘) + 1)) = ((i↑((2 · 𝑘) + 1)) / (3↑((2 · 𝑘) + 1))))
4847oveq2d 7155 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((i↑((2 · 𝑘) + 1)) / (3↑((2 · 𝑘) + 1)))))
49 neg1cn 11743 . . . . . . . . . . . 12 -1 ∈ ℂ
50 expcl 13447 . . . . . . . . . . . 12 ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (-1↑𝑘) ∈ ℂ)
5149, 50mpan 689 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (-1↑𝑘) ∈ ℂ)
52 expcl 13447 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → (i↑((2 · 𝑘) + 1)) ∈ ℂ)
534, 46, 52sylancr 590 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (i↑((2 · 𝑘) + 1)) ∈ ℂ)
54 3nn 11708 . . . . . . . . . . . . 13 3 ∈ ℕ
55 nnexpcl 13442 . . . . . . . . . . . . 13 ((3 ∈ ℕ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → (3↑((2 · 𝑘) + 1)) ∈ ℕ)
5654, 46, 55sylancr 590 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (3↑((2 · 𝑘) + 1)) ∈ ℕ)
5756nncnd 11645 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (3↑((2 · 𝑘) + 1)) ∈ ℂ)
5856nnne0d 11679 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (3↑((2 · 𝑘) + 1)) ≠ 0)
5951, 53, 57, 58divassd 11444 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((i↑((2 · 𝑘) + 1)) / (3↑((2 · 𝑘) + 1)))))
60 expp1 13436 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (2 · 𝑘) ∈ ℕ0) → (i↑((2 · 𝑘) + 1)) = ((i↑(2 · 𝑘)) · i))
614, 44, 60sylancr 590 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (i↑((2 · 𝑘) + 1)) = ((i↑(2 · 𝑘)) · i))
62 expmul 13474 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ 2 ∈ ℕ0𝑘 ∈ ℕ0) → (i↑(2 · 𝑘)) = ((i↑2)↑𝑘))
634, 42, 62mp3an12 1448 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (i↑(2 · 𝑘)) = ((i↑2)↑𝑘))
64 i2 13565 . . . . . . . . . . . . . . . . 17 (i↑2) = -1
6564oveq1i 7149 . . . . . . . . . . . . . . . 16 ((i↑2)↑𝑘) = (-1↑𝑘)
6663, 65eqtrdi 2852 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (i↑(2 · 𝑘)) = (-1↑𝑘))
6766oveq1d 7154 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((i↑(2 · 𝑘)) · i) = ((-1↑𝑘) · i))
6861, 67eqtrd 2836 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (i↑((2 · 𝑘) + 1)) = ((-1↑𝑘) · i))
6968oveq2d 7155 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · (i↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((-1↑𝑘) · i)))
7051, 51, 39mulassd 10657 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (-1↑𝑘)) · i) = ((-1↑𝑘) · ((-1↑𝑘) · i)))
7149a1i 11 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → -1 ∈ ℂ)
72 id 22 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
7371, 72, 72expaddd 13512 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (-1↑(𝑘 + 𝑘)) = ((-1↑𝑘) · (-1↑𝑘)))
74 expmul 13474 . . . . . . . . . . . . . . . . . 18 ((-1 ∈ ℂ ∧ 2 ∈ ℕ0𝑘 ∈ ℕ0) → (-1↑(2 · 𝑘)) = ((-1↑2)↑𝑘))
7549, 42, 74mp3an12 1448 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = ((-1↑2)↑𝑘))
76 neg1sqe1 13559 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
7776oveq1i 7149 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝑘) = (1↑𝑘)
7875, 77eqtrdi 2852 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = (1↑𝑘))
79 nn0cn 11899 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
80792timesd 11872 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0 → (2 · 𝑘) = (𝑘 + 𝑘))
8180oveq2d 7155 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = (-1↑(𝑘 + 𝑘)))
82 nn0z 11997 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
83 1exp 13458 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℤ → (1↑𝑘) = 1)
8482, 83syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (1↑𝑘) = 1)
8578, 81, 843eqtr3d 2844 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (-1↑(𝑘 + 𝑘)) = 1)
8673, 85eqtr3d 2838 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · (-1↑𝑘)) = 1)
8786oveq1d 7154 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (-1↑𝑘)) · i) = (1 · i))
884mulid2i 10639 . . . . . . . . . . . . 13 (1 · i) = i
8987, 88eqtrdi 2852 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (-1↑𝑘)) · i) = i)
9069, 70, 893eqtr2d 2842 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · (i↑((2 · 𝑘) + 1))) = i)
9190oveq1d 7154 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = (i / (3↑((2 · 𝑘) + 1))))
9248, 59, 913eqtr2d 2842 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) = (i / (3↑((2 · 𝑘) + 1))))
9392oveq1d 7154 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((i / (3↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)))
94 expcl 13447 . . . . . . . . . 10 (((i / 3) ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → ((i / 3)↑((2 · 𝑘) + 1)) ∈ ℂ)
9510, 46, 94sylancr 590 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((i / 3)↑((2 · 𝑘) + 1)) ∈ ℂ)
96 nn0p1nn 11928 . . . . . . . . . . 11 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
9744, 96syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
9897nncnd 11645 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℂ)
9997nnne0d 11679 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ≠ 0)
10051, 95, 98, 99divassd 11444 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
10139, 57, 98, 58, 99divdiv1d 11440 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((i / (3↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = (i / ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1))))
10293, 100, 1013eqtr3d 2844 . . . . . . 7 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (i / ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1))))
10357, 98mulcomd 10655 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1)) = (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1))))
104103oveq2d 7155 . . . . . . 7 (𝑘 ∈ ℕ0 → (i / ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1))) = (i / (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1)))))
10538, 102, 1043eqtrd 2840 . . . . . 6 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = (i / (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1)))))
10697, 56nnmulcld 11682 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1))) ∈ ℕ)
107106nncnd 11645 . . . . . . 7 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1))) ∈ ℂ)
108106nnne0d 11679 . . . . . . 7 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1))) ≠ 0)
10939, 107, 108divcld 11409 . . . . . 6 (𝑘 ∈ ℕ0 → (i / (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1)))) ∈ ℂ)
110105, 109eqeltrd 2893 . . . . 5 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) ∈ ℂ)
111110adantl 485 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) ∈ ℂ)
11233oveq2d 7155 . . . . . . . . 9 (𝑛 = 𝑘 → (3 · ((2 · 𝑛) + 1)) = (3 · ((2 · 𝑘) + 1)))
113 oveq2 7147 . . . . . . . . 9 (𝑛 = 𝑘 → (9↑𝑛) = (9↑𝑘))
114112, 113oveq12d 7157 . . . . . . . 8 (𝑛 = 𝑘 → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) = ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))
115114oveq2d 7155 . . . . . . 7 (𝑛 = 𝑘 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
116 log2cnv.1 . . . . . . 7 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
117 ovex 7172 . . . . . . 7 (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) ∈ V
118115, 116, 117fvmpt 6749 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐹𝑘) = (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
119 expp1 13436 . . . . . . . . . . . . . . 15 ((3 ∈ ℂ ∧ (2 · 𝑘) ∈ ℕ0) → (3↑((2 · 𝑘) + 1)) = ((3↑(2 · 𝑘)) · 3))
1208, 44, 119sylancr 590 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (3↑((2 · 𝑘) + 1)) = ((3↑(2 · 𝑘)) · 3))
121 expmul 13474 . . . . . . . . . . . . . . . . 17 ((3 ∈ ℂ ∧ 2 ∈ ℕ0𝑘 ∈ ℕ0) → (3↑(2 · 𝑘)) = ((3↑2)↑𝑘))
1228, 42, 121mp3an12 1448 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (3↑(2 · 𝑘)) = ((3↑2)↑𝑘))
123 sq3 13561 . . . . . . . . . . . . . . . . 17 (3↑2) = 9
124123oveq1i 7149 . . . . . . . . . . . . . . . 16 ((3↑2)↑𝑘) = (9↑𝑘)
125122, 124eqtrdi 2852 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (3↑(2 · 𝑘)) = (9↑𝑘))
126125oveq1d 7154 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((3↑(2 · 𝑘)) · 3) = ((9↑𝑘) · 3))
127 9nn 11727 . . . . . . . . . . . . . . . . 17 9 ∈ ℕ
128 nnexpcl 13442 . . . . . . . . . . . . . . . . 17 ((9 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (9↑𝑘) ∈ ℕ)
129127, 128mpan 689 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (9↑𝑘) ∈ ℕ)
130129nncnd 11645 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (9↑𝑘) ∈ ℂ)
131 mulcom 10616 . . . . . . . . . . . . . . 15 (((9↑𝑘) ∈ ℂ ∧ 3 ∈ ℂ) → ((9↑𝑘) · 3) = (3 · (9↑𝑘)))
132130, 8, 131sylancl 589 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((9↑𝑘) · 3) = (3 · (9↑𝑘)))
133120, 126, 1323eqtrd 2840 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (3↑((2 · 𝑘) + 1)) = (3 · (9↑𝑘)))
13490, 133oveq12d 7157 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = (i / (3 · (9↑𝑘))))
13548, 59, 1343eqtr2d 2842 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) = (i / (3 · (9↑𝑘))))
136135oveq1d 7154 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (((-1↑𝑘) · ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((i / (3 · (9↑𝑘))) / ((2 · 𝑘) + 1)))
137 nnmulcl 11653 . . . . . . . . . . . . 13 ((3 ∈ ℕ ∧ (9↑𝑘) ∈ ℕ) → (3 · (9↑𝑘)) ∈ ℕ)
13854, 129, 137sylancr 590 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (3 · (9↑𝑘)) ∈ ℕ)
139138nncnd 11645 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (3 · (9↑𝑘)) ∈ ℂ)
140138nnne0d 11679 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (3 · (9↑𝑘)) ≠ 0)
14139, 139, 98, 140, 99divdiv1d 11440 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((i / (3 · (9↑𝑘))) / ((2 · 𝑘) + 1)) = (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1))))
142136, 100, 1413eqtr3d 2844 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1))))
14340, 130, 98mul32d 10843 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1)) = ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))
144143oveq2d 7155 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1))) = (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
14538, 142, 1443eqtrd 2840 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
146145oveq2d 7155 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 / i) · ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘)) = ((2 / i) · (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))))
147 nnmulcl 11653 . . . . . . . . . . . 12 ((3 ∈ ℕ ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (3 · ((2 · 𝑘) + 1)) ∈ ℕ)
14854, 97, 147sylancr 590 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (3 · ((2 · 𝑘) + 1)) ∈ ℕ)
149148, 129nnmulcld 11682 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ∈ ℕ)
150149nncnd 11645 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ∈ ℂ)
151149nnne0d 11679 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ≠ 0)
15239, 150, 151divcld 11409 . . . . . . . 8 (𝑘 ∈ ℕ0 → (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) ∈ ℂ)
153 mulcom 10616 . . . . . . . 8 (((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) ∈ ℂ ∧ (2 / i) ∈ ℂ) → ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = ((2 / i) · (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))))
154152, 6, 153sylancl 589 . . . . . . 7 (𝑘 ∈ ℕ0 → ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = ((2 / i) · (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))))
1553a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℂ)
1565a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → i ≠ 0)
157155, 39, 150, 156, 151dmdcand 11438 . . . . . . 7 (𝑘 ∈ ℕ0 → ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
158146, 154, 1573eqtr2d 2842 . . . . . 6 (𝑘 ∈ ℕ0 → ((2 / i) · ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘)) = (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
159118, 158eqtr4d 2839 . . . . 5 (𝑘 ∈ ℕ0 → (𝐹𝑘) = ((2 / i) · ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘)))
160159adantl 485 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐹𝑘) = ((2 / i) · ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘)))
1611, 2, 7, 30, 111, 160isermulc2 15010 . . 3 (⊤ → seq0( + , 𝐹) ⇝ ((2 / i) · (arctan‘(i / 3))))
162161mptru 1545 . 2 seq0( + , 𝐹) ⇝ ((2 / i) · (arctan‘(i / 3)))
163 bndatandm 25519 . . . . . . . 8 (((i / 3) ∈ ℂ ∧ (abs‘(i / 3)) < 1) → (i / 3) ∈ dom arctan)
16410, 26, 163mp2an 691 . . . . . . 7 (i / 3) ∈ dom arctan
165 atanval 25474 . . . . . . 7 ((i / 3) ∈ dom arctan → (arctan‘(i / 3)) = ((i / 2) · ((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i · (i / 3)))))))
166164, 165ax-mp 5 . . . . . 6 (arctan‘(i / 3)) = ((i / 2) · ((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i · (i / 3))))))
167 df-4 11694 . . . . . . . . . . . . 13 4 = (3 + 1)
168167oveq1i 7149 . . . . . . . . . . . 12 (4 / 3) = ((3 + 1) / 3)
169 ax-1cn 10588 . . . . . . . . . . . . 13 1 ∈ ℂ
1708, 169, 8, 9divdiri 11390 . . . . . . . . . . . 12 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
1718, 9dividi 11366 . . . . . . . . . . . . 13 (3 / 3) = 1
172171oveq1i 7149 . . . . . . . . . . . 12 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
173168, 170, 1723eqtri 2828 . . . . . . . . . . 11 (4 / 3) = (1 + (1 / 3))
174169, 8, 9divcli 11375 . . . . . . . . . . . 12 (1 / 3) ∈ ℂ
175169, 174subnegi 10958 . . . . . . . . . . 11 (1 − -(1 / 3)) = (1 + (1 / 3))
176 divneg 11325 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → -(1 / 3) = (-1 / 3))
177169, 8, 9, 176mp3an 1458 . . . . . . . . . . . . 13 -(1 / 3) = (-1 / 3)
178 ixi 11262 . . . . . . . . . . . . . 14 (i · i) = -1
179178oveq1i 7149 . . . . . . . . . . . . 13 ((i · i) / 3) = (-1 / 3)
1804, 4, 8, 9divassi 11389 . . . . . . . . . . . . 13 ((i · i) / 3) = (i · (i / 3))
181177, 179, 1803eqtr2i 2830 . . . . . . . . . . . 12 -(1 / 3) = (i · (i / 3))
182181oveq2i 7150 . . . . . . . . . . 11 (1 − -(1 / 3)) = (1 − (i · (i / 3)))
183173, 175, 1823eqtr2ri 2831 . . . . . . . . . 10 (1 − (i · (i / 3))) = (4 / 3)
184183fveq2i 6652 . . . . . . . . 9 (log‘(1 − (i · (i / 3)))) = (log‘(4 / 3))
1858, 9pm3.2i 474 . . . . . . . . . . . . 13 (3 ∈ ℂ ∧ 3 ≠ 0)
186 divsubdir 11327 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((3 − 1) / 3) = ((3 / 3) − (1 / 3)))
1878, 169, 185, 186mp3an 1458 . . . . . . . . . . . 12 ((3 − 1) / 3) = ((3 / 3) − (1 / 3))
188 3m1e2 11757 . . . . . . . . . . . . 13 (3 − 1) = 2
189188oveq1i 7149 . . . . . . . . . . . 12 ((3 − 1) / 3) = (2 / 3)
190171oveq1i 7149 . . . . . . . . . . . 12 ((3 / 3) − (1 / 3)) = (1 − (1 / 3))
191187, 189, 1903eqtr3i 2832 . . . . . . . . . . 11 (2 / 3) = (1 − (1 / 3))
192169, 174negsubi 10957 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 − (1 / 3))
193181oveq2i 7150 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 + (i · (i / 3)))
194191, 192, 1933eqtr2ri 2831 . . . . . . . . . 10 (1 + (i · (i / 3))) = (2 / 3)
195194fveq2i 6652 . . . . . . . . 9 (log‘(1 + (i · (i / 3)))) = (log‘(2 / 3))
196184, 195oveq12i 7151 . . . . . . . 8 ((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i · (i / 3))))) = ((log‘(4 / 3)) − (log‘(2 / 3)))
197 4re 11713 . . . . . . . . . . 11 4 ∈ ℝ
198 4pos 11736 . . . . . . . . . . 11 0 < 4
199197, 198elrpii 12384 . . . . . . . . . 10 4 ∈ ℝ+
200 3rp 12387 . . . . . . . . . 10 3 ∈ ℝ+
201 rpdivcl 12406 . . . . . . . . . 10 ((4 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (4 / 3) ∈ ℝ+)
202199, 200, 201mp2an 691 . . . . . . . . 9 (4 / 3) ∈ ℝ+
203 2rp 12386 . . . . . . . . . 10 2 ∈ ℝ+
204 rpdivcl 12406 . . . . . . . . . 10 ((2 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (2 / 3) ∈ ℝ+)
205203, 200, 204mp2an 691 . . . . . . . . 9 (2 / 3) ∈ ℝ+
206 relogdiv 25188 . . . . . . . . 9 (((4 / 3) ∈ ℝ+ ∧ (2 / 3) ∈ ℝ+) → (log‘((4 / 3) / (2 / 3))) = ((log‘(4 / 3)) − (log‘(2 / 3))))
207202, 205, 206mp2an 691 . . . . . . . 8 (log‘((4 / 3) / (2 / 3))) = ((log‘(4 / 3)) − (log‘(2 / 3)))
208 4cn 11714 . . . . . . . . . . 11 4 ∈ ℂ
209 2cnne0 11839 . . . . . . . . . . 11 (2 ∈ ℂ ∧ 2 ≠ 0)
210 divcan7 11342 . . . . . . . . . . 11 ((4 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((4 / 3) / (2 / 3)) = (4 / 2))
211208, 209, 185, 210mp3an 1458 . . . . . . . . . 10 ((4 / 3) / (2 / 3)) = (4 / 2)
212 4d2e2 11799 . . . . . . . . . 10 (4 / 2) = 2
213211, 212eqtri 2824 . . . . . . . . 9 ((4 / 3) / (2 / 3)) = 2
214213fveq2i 6652 . . . . . . . 8 (log‘((4 / 3) / (2 / 3))) = (log‘2)
215196, 207, 2143eqtr2i 2830 . . . . . . 7 ((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i · (i / 3))))) = (log‘2)
216215oveq2i 7150 . . . . . 6 ((i / 2) · ((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i · (i / 3)))))) = ((i / 2) · (log‘2))
217166, 216eqtri 2824 . . . . 5 (arctan‘(i / 3)) = ((i / 2) · (log‘2))
218217oveq2i 7150 . . . 4 ((2 / i) · (arctan‘(i / 3))) = ((2 / i) · ((i / 2) · (log‘2)))
219 2ne0 11733 . . . . . 6 2 ≠ 0
2204, 3, 219divcli 11375 . . . . 5 (i / 2) ∈ ℂ
221 logcl 25164 . . . . . 6 ((2 ∈ ℂ ∧ 2 ≠ 0) → (log‘2) ∈ ℂ)
2223, 219, 221mp2an 691 . . . . 5 (log‘2) ∈ ℂ
2236, 220, 222mulassi 10645 . . . 4 (((2 / i) · (i / 2)) · (log‘2)) = ((2 / i) · ((i / 2) · (log‘2)))
224218, 223eqtr4i 2827 . . 3 ((2 / i) · (arctan‘(i / 3))) = (((2 / i) · (i / 2)) · (log‘2))
225 divcan6 11340 . . . . 5 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((2 / i) · (i / 2)) = 1)
2263, 219, 4, 5, 225mp4an 692 . . . 4 ((2 / i) · (i / 2)) = 1
227226oveq1i 7149 . . 3 (((2 / i) · (i / 2)) · (log‘2)) = (1 · (log‘2))
228222mulid2i 10639 . . 3 (1 · (log‘2)) = (log‘2)
229224, 227, 2283eqtri 2828 . 2 ((2 / i) · (arctan‘(i / 3))) = (log‘2)
230162, 229breqtri 5058 1 seq0( + , 𝐹) ⇝ (log‘2)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ⊤wtru 1539   ∈ wcel 2112   ≠ wne 2990   class class class wbr 5033   ↦ cmpt 5113  dom cdm 5523  ‘cfv 6328  (class class class)co 7139  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531  ici 10532   + caddc 10533   · cmul 10535   < clt 10668   ≤ cle 10669   − cmin 10863  -cneg 10864   / cdiv 11290  ℕcn 11629  2c2 11684  3c3 11685  4c4 11686  9c9 11691  ℕ0cn0 11889  ℤcz 11973  ℝ+crp 12381  seqcseq 13368  ↑cexp 13429  abscabs 14589   ⇝ cli 14837  logclog 25150  arctancatan 25454 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13430  df-fac 13634  df-bc 13663  df-hash 13691  df-shft 14422  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-sum 15039  df-ef 15417  df-sin 15419  df-cos 15420  df-tan 15421  df-pi 15422  df-dvds 15604  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cld 21628  df-ntr 21629  df-cls 21630  df-nei 21707  df-lp 21745  df-perf 21746  df-cn 21836  df-cnp 21837  df-haus 21924  df-cmp 21996  df-tx 22171  df-hmeo 22364  df-fil 22455  df-fm 22547  df-flim 22548  df-flf 22549  df-xms 22931  df-ms 22932  df-tms 22933  df-cncf 23487  df-limc 24473  df-dv 24474  df-ulm 24976  df-log 25152  df-atan 25457 This theorem is referenced by:  log2tlbnd  25535
 Copyright terms: Public domain W3C validator