| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | 0zd 12625 |
. . . 4
⊢ (⊤
→ 0 ∈ ℤ) |
| 3 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 4 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 5 | | ine0 11698 |
. . . . . 6
⊢ i ≠
0 |
| 6 | 3, 4, 5 | divcli 12009 |
. . . . 5
⊢ (2 / i)
∈ ℂ |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (⊤
→ (2 / i) ∈ ℂ) |
| 8 | | 3cn 12347 |
. . . . . . 7
⊢ 3 ∈
ℂ |
| 9 | | 3ne0 12372 |
. . . . . . 7
⊢ 3 ≠
0 |
| 10 | 4, 8, 9 | divcli 12009 |
. . . . . 6
⊢ (i / 3)
∈ ℂ |
| 11 | | absdiv 15334 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (abs‘(i /
3)) = ((abs‘i) / (abs‘3))) |
| 12 | 4, 8, 9, 11 | mp3an 1463 |
. . . . . . . 8
⊢
(abs‘(i / 3)) = ((abs‘i) / (abs‘3)) |
| 13 | | absi 15325 |
. . . . . . . . 9
⊢
(abs‘i) = 1 |
| 14 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 15 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 16 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 17 | 15, 14, 16 | ltleii 11384 |
. . . . . . . . . 10
⊢ 0 ≤
3 |
| 18 | | absid 15335 |
. . . . . . . . . 10
⊢ ((3
∈ ℝ ∧ 0 ≤ 3) → (abs‘3) = 3) |
| 19 | 14, 17, 18 | mp2an 692 |
. . . . . . . . 9
⊢
(abs‘3) = 3 |
| 20 | 13, 19 | oveq12i 7443 |
. . . . . . . 8
⊢
((abs‘i) / (abs‘3)) = (1 / 3) |
| 21 | 12, 20 | eqtri 2765 |
. . . . . . 7
⊢
(abs‘(i / 3)) = (1 / 3) |
| 22 | | 1lt3 12439 |
. . . . . . . 8
⊢ 1 <
3 |
| 23 | | recgt1 12164 |
. . . . . . . . 9
⊢ ((3
∈ ℝ ∧ 0 < 3) → (1 < 3 ↔ (1 / 3) <
1)) |
| 24 | 14, 16, 23 | mp2an 692 |
. . . . . . . 8
⊢ (1 < 3
↔ (1 / 3) < 1) |
| 25 | 22, 24 | mpbi 230 |
. . . . . . 7
⊢ (1 / 3)
< 1 |
| 26 | 21, 25 | eqbrtri 5164 |
. . . . . 6
⊢
(abs‘(i / 3)) < 1 |
| 27 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((-1↑𝑛)
· (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ0 ↦
((-1↑𝑛) · (((i
/ 3)↑((2 · 𝑛) +
1)) / ((2 · 𝑛) +
1)))) |
| 28 | 27 | atantayl3 26982 |
. . . . . 6
⊢ (((i / 3)
∈ ℂ ∧ (abs‘(i / 3)) < 1) → seq0( + , (𝑛 ∈ ℕ0
↦ ((-1↑𝑛)
· (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝ (arctan‘(i /
3))) |
| 29 | 10, 26, 28 | mp2an 692 |
. . . . 5
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝
(arctan‘(i / 3)) |
| 30 | 29 | a1i 11 |
. . . 4
⊢ (⊤
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝
(arctan‘(i / 3))) |
| 31 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (-1↑𝑛) = (-1↑𝑘)) |
| 32 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘)) |
| 33 | 32 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1)) |
| 34 | 33 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((i / 3)↑((2 · 𝑛) + 1)) = ((i / 3)↑((2
· 𝑘) +
1))) |
| 35 | 34, 33 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)) = (((i / 3)↑((2
· 𝑘) + 1)) / ((2
· 𝑘) +
1))) |
| 36 | 31, 35 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) = ((-1↑𝑘) · (((i / 3)↑((2
· 𝑘) + 1)) / ((2
· 𝑘) +
1)))) |
| 37 | | ovex 7464 |
. . . . . . . 8
⊢
((-1↑𝑘)
· (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ V |
| 38 | 36, 27, 37 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
| 39 | 4 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ i ∈ ℂ) |
| 40 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 3 ∈ ℂ) |
| 41 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 3 ≠ 0) |
| 42 | | 2nn0 12543 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
| 43 | | nn0mulcl 12562 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ0 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
| 44 | 42, 43 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℕ0) |
| 45 | | peano2nn0 12566 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑘) ∈
ℕ0 → ((2 · 𝑘) + 1) ∈
ℕ0) |
| 46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
| 47 | 39, 40, 41, 46 | expdivd 14200 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((i / 3)↑((2 · 𝑘) + 1)) = ((i↑((2 · 𝑘) + 1)) / (3↑((2 ·
𝑘) + 1)))) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((i↑((2 · 𝑘) + 1)) / (3↑((2 ·
𝑘) +
1))))) |
| 49 | | neg1cn 12380 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℂ |
| 50 | | expcl 14120 |
. . . . . . . . . . . 12
⊢ ((-1
∈ ℂ ∧ 𝑘
∈ ℕ0) → (-1↑𝑘) ∈ ℂ) |
| 51 | 49, 50 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (-1↑𝑘) ∈
ℂ) |
| 52 | | expcl 14120 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(i↑((2 · 𝑘) +
1)) ∈ ℂ) |
| 53 | 4, 46, 52 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (i↑((2 · 𝑘) + 1)) ∈ ℂ) |
| 54 | | 3nn 12345 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ |
| 55 | | nnexpcl 14115 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℕ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(3↑((2 · 𝑘) +
1)) ∈ ℕ) |
| 56 | 54, 46, 55 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (3↑((2 · 𝑘) + 1)) ∈ ℕ) |
| 57 | 56 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (3↑((2 · 𝑘) + 1)) ∈ ℂ) |
| 58 | 56 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (3↑((2 · 𝑘) + 1)) ≠ 0) |
| 59 | 51, 53, 57, 58 | divassd 12078 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((i↑((2 ·
𝑘) + 1)) / (3↑((2
· 𝑘) +
1))))) |
| 60 | | expp1 14109 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ (2 · 𝑘) ∈ ℕ0) →
(i↑((2 · 𝑘) +
1)) = ((i↑(2 · 𝑘)) · i)) |
| 61 | 4, 44, 60 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (i↑((2 · 𝑘) + 1)) = ((i↑(2 · 𝑘)) · i)) |
| 62 | | expmul 14148 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0) →
(i↑(2 · 𝑘)) =
((i↑2)↑𝑘)) |
| 63 | 4, 42, 62 | mp3an12 1453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (i↑(2 · 𝑘)) = ((i↑2)↑𝑘)) |
| 64 | | i2 14241 |
. . . . . . . . . . . . . . . . 17
⊢
(i↑2) = -1 |
| 65 | 64 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢
((i↑2)↑𝑘)
= (-1↑𝑘) |
| 66 | 63, 65 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (i↑(2 · 𝑘)) = (-1↑𝑘)) |
| 67 | 66 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((i↑(2 · 𝑘)) · i) = ((-1↑𝑘) · i)) |
| 68 | 61, 67 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (i↑((2 · 𝑘) + 1)) = ((-1↑𝑘) · i)) |
| 69 | 68 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· (i↑((2 · 𝑘) + 1))) = ((-1↑𝑘) · ((-1↑𝑘) · i))) |
| 70 | 51, 51, 39 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (-1↑𝑘))
· i) = ((-1↑𝑘)
· ((-1↑𝑘)
· i))) |
| 71 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ -1 ∈ ℂ) |
| 72 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) |
| 73 | 71, 72, 72 | expaddd 14188 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (-1↑(𝑘 + 𝑘)) = ((-1↑𝑘) · (-1↑𝑘))) |
| 74 | | expmul 14148 |
. . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0) →
(-1↑(2 · 𝑘)) =
((-1↑2)↑𝑘)) |
| 75 | 49, 42, 74 | mp3an12 1453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ (-1↑(2 · 𝑘)) = ((-1↑2)↑𝑘)) |
| 76 | | neg1sqe1 14235 |
. . . . . . . . . . . . . . . . . 18
⊢
(-1↑2) = 1 |
| 77 | 76 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢
((-1↑2)↑𝑘)
= (1↑𝑘) |
| 78 | 75, 77 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (-1↑(2 · 𝑘)) = (1↑𝑘)) |
| 79 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
| 80 | 79 | 2timesd 12509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘) =
(𝑘 + 𝑘)) |
| 81 | 80 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (-1↑(2 · 𝑘)) = (-1↑(𝑘 + 𝑘))) |
| 82 | | nn0z 12638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
| 83 | | 1exp 14132 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ →
(1↑𝑘) =
1) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (1↑𝑘) =
1) |
| 85 | 78, 81, 84 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (-1↑(𝑘 + 𝑘)) = 1) |
| 86 | 73, 85 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· (-1↑𝑘)) =
1) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (-1↑𝑘))
· i) = (1 · i)) |
| 88 | 4 | mullidi 11266 |
. . . . . . . . . . . . 13
⊢ (1
· i) = i |
| 89 | 87, 88 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (-1↑𝑘))
· i) = i) |
| 90 | 69, 70, 89 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· (i↑((2 · 𝑘) + 1))) = i) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = (i / (3↑((2
· 𝑘) +
1)))) |
| 92 | 48, 59, 91 | 3eqtr2d 2783 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) = (i / (3↑((2 · 𝑘) + 1)))) |
| 93 | 92 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((i / (3↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1))) |
| 94 | | expcl 14120 |
. . . . . . . . . 10
⊢ (((i / 3)
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → ((i
/ 3)↑((2 · 𝑘) +
1)) ∈ ℂ) |
| 95 | 10, 46, 94 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((i / 3)↑((2 · 𝑘) + 1)) ∈ ℂ) |
| 96 | | nn0p1nn 12565 |
. . . . . . . . . . 11
⊢ ((2
· 𝑘) ∈
ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ) |
| 97 | 44, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℕ) |
| 98 | 97 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℂ) |
| 99 | 97 | nnne0d 12316 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
≠ 0) |
| 100 | 51, 95, 98, 99 | divassd 12078 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((-1↑𝑘) · (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
| 101 | 39, 57, 98, 58, 99 | divdiv1d 12074 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((i / (3↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = (i / ((3↑((2 · 𝑘) + 1)) · ((2 ·
𝑘) + 1)))) |
| 102 | 93, 100, 101 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (i / ((3↑((2 · 𝑘) + 1)) · ((2 ·
𝑘) + 1)))) |
| 103 | 57, 98 | mulcomd 11282 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1)) = (((2 · 𝑘) + 1) · (3↑((2
· 𝑘) +
1)))) |
| 104 | 103 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (i / ((3↑((2 · 𝑘) + 1)) · ((2 · 𝑘) + 1))) = (i / (((2 ·
𝑘) + 1) ·
(3↑((2 · 𝑘) +
1))))) |
| 105 | 38, 102, 104 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = (i / (((2 · 𝑘) + 1) · (3↑((2
· 𝑘) +
1))))) |
| 106 | 97, 56 | nnmulcld 12319 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) · (3↑((2 · 𝑘) + 1))) ∈ ℕ) |
| 107 | 106 | nncnd 12282 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) · (3↑((2 · 𝑘) + 1))) ∈ ℂ) |
| 108 | 106 | nnne0d 12316 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) · (3↑((2 · 𝑘) + 1))) ≠ 0) |
| 109 | 39, 107, 108 | divcld 12043 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (i / (((2 · 𝑘) + 1) · (3↑((2 · 𝑘) + 1)))) ∈
ℂ) |
| 110 | 105, 109 | eqeltrd 2841 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) ∈
ℂ) |
| 111 | 110 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) · (((i
/ 3)↑((2 · 𝑛) +
1)) / ((2 · 𝑛) +
1))))‘𝑘) ∈
ℂ) |
| 112 | 33 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (3 · ((2 · 𝑛) + 1)) = (3 · ((2
· 𝑘) +
1))) |
| 113 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (9↑𝑛) = (9↑𝑘)) |
| 114 | 112, 113 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) = ((3 · ((2 ·
𝑘) + 1)) ·
(9↑𝑘))) |
| 115 | 114 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (2 / ((3 · ((2
· 𝑘) + 1)) ·
(9↑𝑘)))) |
| 116 | | log2cnv.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))) |
| 117 | | ovex 7464 |
. . . . . . 7
⊢ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘)))
∈ V |
| 118 | 115, 116,
117 | fvmpt 7016 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = (2 / ((3 · ((2
· 𝑘) + 1)) ·
(9↑𝑘)))) |
| 119 | | expp1 14109 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℂ ∧ (2 · 𝑘) ∈ ℕ0) →
(3↑((2 · 𝑘) +
1)) = ((3↑(2 · 𝑘)) · 3)) |
| 120 | 8, 44, 119 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (3↑((2 · 𝑘) + 1)) = ((3↑(2 · 𝑘)) · 3)) |
| 121 | | expmul 14148 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0) →
(3↑(2 · 𝑘)) =
((3↑2)↑𝑘)) |
| 122 | 8, 42, 121 | mp3an12 1453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (3↑(2 · 𝑘)) = ((3↑2)↑𝑘)) |
| 123 | | sq3 14237 |
. . . . . . . . . . . . . . . . 17
⊢
(3↑2) = 9 |
| 124 | 123 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢
((3↑2)↑𝑘)
= (9↑𝑘) |
| 125 | 122, 124 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (3↑(2 · 𝑘)) = (9↑𝑘)) |
| 126 | 125 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((3↑(2 · 𝑘)) · 3) = ((9↑𝑘) · 3)) |
| 127 | | 9nn 12364 |
. . . . . . . . . . . . . . . . 17
⊢ 9 ∈
ℕ |
| 128 | | nnexpcl 14115 |
. . . . . . . . . . . . . . . . 17
⊢ ((9
∈ ℕ ∧ 𝑘
∈ ℕ0) → (9↑𝑘) ∈ ℕ) |
| 129 | 127, 128 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (9↑𝑘) ∈
ℕ) |
| 130 | 129 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (9↑𝑘) ∈
ℂ) |
| 131 | | mulcom 11241 |
. . . . . . . . . . . . . . 15
⊢
(((9↑𝑘) ∈
ℂ ∧ 3 ∈ ℂ) → ((9↑𝑘) · 3) = (3 · (9↑𝑘))) |
| 132 | 130, 8, 131 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((9↑𝑘) ·
3) = (3 · (9↑𝑘))) |
| 133 | 120, 126,
132 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (3↑((2 · 𝑘) + 1)) = (3 · (9↑𝑘))) |
| 134 | 90, 133 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· (i↑((2 · 𝑘) + 1))) / (3↑((2 · 𝑘) + 1))) = (i / (3 ·
(9↑𝑘)))) |
| 135 | 48, 59, 134 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) = (i / (3 · (9↑𝑘)))) |
| 136 | 135 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (((-1↑𝑘)
· ((i / 3)↑((2 · 𝑘) + 1))) / ((2 · 𝑘) + 1)) = ((i / (3 · (9↑𝑘))) / ((2 · 𝑘) + 1))) |
| 137 | | nnmulcl 12290 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℕ ∧ (9↑𝑘) ∈ ℕ) → (3 ·
(9↑𝑘)) ∈
ℕ) |
| 138 | 54, 129, 137 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (3 · (9↑𝑘)) ∈ ℕ) |
| 139 | 138 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (3 · (9↑𝑘)) ∈ ℂ) |
| 140 | 138 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (3 · (9↑𝑘)) ≠ 0) |
| 141 | 39, 139, 98, 140, 99 | divdiv1d 12074 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((i / (3 · (9↑𝑘))) / ((2 · 𝑘) + 1)) = (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1)))) |
| 142 | 136, 100,
141 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘)
· (((i / 3)↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1)))) |
| 143 | 40, 130, 98 | mul32d 11471 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1)) = ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (i / ((3 · (9↑𝑘)) · ((2 · 𝑘) + 1))) = (i / ((3 · ((2 ·
𝑘) + 1)) ·
(9↑𝑘)))) |
| 145 | 38, 142, 144 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘) = (i / ((3 · ((2
· 𝑘) + 1)) ·
(9↑𝑘)))) |
| 146 | 145 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((2 / i) · ((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) · (((i
/ 3)↑((2 · 𝑛) +
1)) / ((2 · 𝑛) +
1))))‘𝑘)) = ((2 / i)
· (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) |
| 147 | | nnmulcl 12290 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℕ ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (3 · ((2
· 𝑘) + 1)) ∈
ℕ) |
| 148 | 54, 97, 147 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (3 · ((2 · 𝑘) + 1)) ∈ ℕ) |
| 149 | 148, 129 | nnmulcld 12319 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ∈ ℕ) |
| 150 | 149 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ∈ ℂ) |
| 151 | 149 | nnne0d 12316 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) ≠ 0) |
| 152 | 39, 150, 151 | divcld 12043 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) ∈ ℂ) |
| 153 | | mulcom 11241 |
. . . . . . . 8
⊢ (((i /
((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) ∈ ℂ ∧ (2 / i) ∈
ℂ) → ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = ((2 / i) · (i
/ ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) |
| 154 | 152, 6, 153 | sylancl 586 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = ((2 / i) · (i
/ ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) |
| 155 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℂ) |
| 156 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ i ≠ 0) |
| 157 | 155, 39, 150, 156, 151 | dmdcand 12072 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((i / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) · (2 / i)) = (2 / ((3 · ((2
· 𝑘) + 1)) ·
(9↑𝑘)))) |
| 158 | 146, 154,
157 | 3eqtr2d 2783 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((2 / i) · ((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) · (((i
/ 3)↑((2 · 𝑛) +
1)) / ((2 · 𝑛) +
1))))‘𝑘)) = (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘)))) |
| 159 | 118, 158 | eqtr4d 2780 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((2 / i) · ((𝑛 ∈ ℕ0
↦ ((-1↑𝑛)
· (((i / 3)↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))‘𝑘))) |
| 160 | 159 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (𝐹‘𝑘) = ((2 / i) · ((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) · (((i
/ 3)↑((2 · 𝑛) +
1)) / ((2 · 𝑛) +
1))))‘𝑘))) |
| 161 | 1, 2, 7, 30, 111, 160 | isermulc2 15694 |
. . 3
⊢ (⊤
→ seq0( + , 𝐹) ⇝
((2 / i) · (arctan‘(i / 3)))) |
| 162 | 161 | mptru 1547 |
. 2
⊢ seq0( + ,
𝐹) ⇝ ((2 / i)
· (arctan‘(i / 3))) |
| 163 | | bndatandm 26972 |
. . . . . . . 8
⊢ (((i / 3)
∈ ℂ ∧ (abs‘(i / 3)) < 1) → (i / 3) ∈ dom
arctan) |
| 164 | 10, 26, 163 | mp2an 692 |
. . . . . . 7
⊢ (i / 3)
∈ dom arctan |
| 165 | | atanval 26927 |
. . . . . . 7
⊢ ((i / 3)
∈ dom arctan → (arctan‘(i / 3)) = ((i / 2) ·
((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i
· (i / 3))))))) |
| 166 | 164, 165 | ax-mp 5 |
. . . . . 6
⊢
(arctan‘(i / 3)) = ((i / 2) · ((log‘(1 − (i
· (i / 3)))) − (log‘(1 + (i · (i /
3)))))) |
| 167 | | df-4 12331 |
. . . . . . . . . . . . 13
⊢ 4 = (3 +
1) |
| 168 | 167 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (4 / 3) =
((3 + 1) / 3) |
| 169 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 170 | 8, 169, 8, 9 | divdiri 12024 |
. . . . . . . . . . . 12
⊢ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
| 171 | 8, 9 | dividi 12000 |
. . . . . . . . . . . . 13
⊢ (3 / 3) =
1 |
| 172 | 171 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
| 173 | 168, 170,
172 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ (4 / 3) =
(1 + (1 / 3)) |
| 174 | 169, 8, 9 | divcli 12009 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℂ |
| 175 | 169, 174 | subnegi 11588 |
. . . . . . . . . . 11
⊢ (1
− -(1 / 3)) = (1 + (1 / 3)) |
| 176 | | divneg 11959 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → -(1 / 3) = (-1 /
3)) |
| 177 | 169, 8, 9, 176 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢ -(1 / 3)
= (-1 / 3) |
| 178 | | ixi 11892 |
. . . . . . . . . . . . . 14
⊢ (i
· i) = -1 |
| 179 | 178 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((i
· i) / 3) = (-1 / 3) |
| 180 | 4, 4, 8, 9 | divassi 12023 |
. . . . . . . . . . . . 13
⊢ ((i
· i) / 3) = (i · (i / 3)) |
| 181 | 177, 179,
180 | 3eqtr2i 2771 |
. . . . . . . . . . . 12
⊢ -(1 / 3)
= (i · (i / 3)) |
| 182 | 181 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (1
− -(1 / 3)) = (1 − (i · (i / 3))) |
| 183 | 173, 175,
182 | 3eqtr2ri 2772 |
. . . . . . . . . 10
⊢ (1
− (i · (i / 3))) = (4 / 3) |
| 184 | 183 | fveq2i 6909 |
. . . . . . . . 9
⊢
(log‘(1 − (i · (i / 3)))) = (log‘(4 /
3)) |
| 185 | 8, 9 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
| 186 | | divsubdir 11961 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((3 − 1) / 3) = ((3 / 3) − (1 / 3))) |
| 187 | 8, 169, 185, 186 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ ((3
− 1) / 3) = ((3 / 3) − (1 / 3)) |
| 188 | | 3m1e2 12394 |
. . . . . . . . . . . . 13
⊢ (3
− 1) = 2 |
| 189 | 188 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((3
− 1) / 3) = (2 / 3) |
| 190 | 171 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((3 / 3)
− (1 / 3)) = (1 − (1 / 3)) |
| 191 | 187, 189,
190 | 3eqtr3i 2773 |
. . . . . . . . . . 11
⊢ (2 / 3) =
(1 − (1 / 3)) |
| 192 | 169, 174 | negsubi 11587 |
. . . . . . . . . . 11
⊢ (1 + -(1
/ 3)) = (1 − (1 / 3)) |
| 193 | 181 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (1 + -(1
/ 3)) = (1 + (i · (i / 3))) |
| 194 | 191, 192,
193 | 3eqtr2ri 2772 |
. . . . . . . . . 10
⊢ (1 + (i
· (i / 3))) = (2 / 3) |
| 195 | 194 | fveq2i 6909 |
. . . . . . . . 9
⊢
(log‘(1 + (i · (i / 3)))) = (log‘(2 /
3)) |
| 196 | 184, 195 | oveq12i 7443 |
. . . . . . . 8
⊢
((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i
· (i / 3))))) = ((log‘(4 / 3)) − (log‘(2 /
3))) |
| 197 | | 4re 12350 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
| 198 | | 4pos 12373 |
. . . . . . . . . . 11
⊢ 0 <
4 |
| 199 | 197, 198 | elrpii 13037 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
| 200 | | 3rp 13040 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
| 201 | | rpdivcl 13060 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ+ ∧ 3 ∈ ℝ+) → (4 / 3)
∈ ℝ+) |
| 202 | 199, 200,
201 | mp2an 692 |
. . . . . . . . 9
⊢ (4 / 3)
∈ ℝ+ |
| 203 | | 2rp 13039 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
| 204 | | rpdivcl 13060 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ+ ∧ 3 ∈ ℝ+) → (2 / 3)
∈ ℝ+) |
| 205 | 203, 200,
204 | mp2an 692 |
. . . . . . . . 9
⊢ (2 / 3)
∈ ℝ+ |
| 206 | | relogdiv 26635 |
. . . . . . . . 9
⊢ (((4 / 3)
∈ ℝ+ ∧ (2 / 3) ∈ ℝ+) →
(log‘((4 / 3) / (2 / 3))) = ((log‘(4 / 3)) − (log‘(2 /
3)))) |
| 207 | 202, 205,
206 | mp2an 692 |
. . . . . . . 8
⊢
(log‘((4 / 3) / (2 / 3))) = ((log‘(4 / 3)) −
(log‘(2 / 3))) |
| 208 | | 4cn 12351 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
| 209 | | 2cnne0 12476 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 210 | | divcan7 11976 |
. . . . . . . . . . 11
⊢ ((4
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ
∧ 3 ≠ 0)) → ((4 / 3) / (2 / 3)) = (4 / 2)) |
| 211 | 208, 209,
185, 210 | mp3an 1463 |
. . . . . . . . . 10
⊢ ((4 / 3)
/ (2 / 3)) = (4 / 2) |
| 212 | | 4d2e2 12436 |
. . . . . . . . . 10
⊢ (4 / 2) =
2 |
| 213 | 211, 212 | eqtri 2765 |
. . . . . . . . 9
⊢ ((4 / 3)
/ (2 / 3)) = 2 |
| 214 | 213 | fveq2i 6909 |
. . . . . . . 8
⊢
(log‘((4 / 3) / (2 / 3))) = (log‘2) |
| 215 | 196, 207,
214 | 3eqtr2i 2771 |
. . . . . . 7
⊢
((log‘(1 − (i · (i / 3)))) − (log‘(1 + (i
· (i / 3))))) = (log‘2) |
| 216 | 215 | oveq2i 7442 |
. . . . . 6
⊢ ((i / 2)
· ((log‘(1 − (i · (i / 3)))) − (log‘(1 +
(i · (i / 3)))))) = ((i / 2) · (log‘2)) |
| 217 | 166, 216 | eqtri 2765 |
. . . . 5
⊢
(arctan‘(i / 3)) = ((i / 2) ·
(log‘2)) |
| 218 | 217 | oveq2i 7442 |
. . . 4
⊢ ((2 / i)
· (arctan‘(i / 3))) = ((2 / i) · ((i / 2) ·
(log‘2))) |
| 219 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 220 | 4, 3, 219 | divcli 12009 |
. . . . 5
⊢ (i / 2)
∈ ℂ |
| 221 | | logcl 26610 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ 2 ≠ 0) → (log‘2) ∈
ℂ) |
| 222 | 3, 219, 221 | mp2an 692 |
. . . . 5
⊢
(log‘2) ∈ ℂ |
| 223 | 6, 220, 222 | mulassi 11272 |
. . . 4
⊢ (((2 / i)
· (i / 2)) · (log‘2)) = ((2 / i) · ((i / 2) ·
(log‘2))) |
| 224 | 218, 223 | eqtr4i 2768 |
. . 3
⊢ ((2 / i)
· (arctan‘(i / 3))) = (((2 / i) · (i / 2)) ·
(log‘2)) |
| 225 | | divcan6 11974 |
. . . . 5
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) →
((2 / i) · (i / 2)) = 1) |
| 226 | 3, 219, 4, 5, 225 | mp4an 693 |
. . . 4
⊢ ((2 / i)
· (i / 2)) = 1 |
| 227 | 226 | oveq1i 7441 |
. . 3
⊢ (((2 / i)
· (i / 2)) · (log‘2)) = (1 ·
(log‘2)) |
| 228 | 222 | mullidi 11266 |
. . 3
⊢ (1
· (log‘2)) = (log‘2) |
| 229 | 224, 227,
228 | 3eqtri 2769 |
. 2
⊢ ((2 / i)
· (arctan‘(i / 3))) = (log‘2) |
| 230 | 162, 229 | breqtri 5168 |
1
⊢ seq0( + ,
𝐹) ⇝
(log‘2) |