| Step | Hyp | Ref
| Expression |
| 1 | | atantayl3.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
((-1↑𝑛) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
| 2 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 3 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
| 4 | | nn0mulcl 12562 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
| 5 | 2, 3, 4 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (2 · 𝑛) ∈
ℕ0) |
| 6 | 5 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (2 · 𝑛) ∈ ℂ) |
| 7 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 8 | | pncan 11514 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
| 9 | 6, 7, 8 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
| 10 | 9 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((((2 · 𝑛) + 1) − 1) / 2) = ((2 · 𝑛) / 2)) |
| 11 | | nn0cn 12536 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
| 12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 ∈ ℂ) |
| 13 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 2 ∈ ℂ) |
| 14 | | 2ne0 12370 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
| 15 | 14 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 2 ≠ 0) |
| 16 | 12, 13, 15 | divcan3d 12048 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) / 2) = 𝑛) |
| 17 | 10, 16 | eqtr2d 2778 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 = ((((2 · 𝑛) + 1) − 1) / 2)) |
| 18 | 17 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (-1↑𝑛) = (-1↑((((2 · 𝑛) + 1) − 1) /
2))) |
| 19 | 18 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) = ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
| 20 | 19 | mpteq2dva 5242 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ0 ↦
((-1↑((((2 · 𝑛)
+ 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) |
| 21 | 1, 20 | eqtrid 2789 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐹 = (𝑛 ∈ ℕ0
↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) |
| 22 | 21 | seqeq3d 14050 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) = seq0(
+ , (𝑛 ∈
ℕ0 ↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))))) |
| 23 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦ if(2
∥ 𝑘, 0,
((-1↑((𝑘 − 1) /
2)) · ((𝐴↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) ·
((𝐴↑𝑘) / 𝑘)))) |
| 24 | 23 | atantayl2 26981 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑘 ∈
ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · ((𝐴↑𝑘) / 𝑘))))) ⇝ (arctan‘𝐴)) |
| 25 | | neg1cn 12380 |
. . . . . . 7
⊢ -1 ∈
ℂ |
| 26 | | expcl 14120 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ 𝑛
∈ ℕ0) → (-1↑𝑛) ∈ ℂ) |
| 27 | 25, 3, 26 | sylancr 587 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (-1↑𝑛) ∈ ℂ) |
| 28 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝐴 ∈ ℂ) |
| 29 | | peano2nn0 12566 |
. . . . . . . . 9
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈
ℕ0) |
| 30 | 5, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈
ℕ0) |
| 31 | 28, 30 | expcld 14186 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (𝐴↑((2 · 𝑛) + 1)) ∈ ℂ) |
| 32 | | nn0p1nn 12565 |
. . . . . . . . 9
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ) |
| 33 | 5, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ) |
| 34 | 33 | nncnd 12282 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈ ℂ) |
| 35 | 33 | nnne0d 12316 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ≠ 0) |
| 36 | 31, 34, 35 | divcld 12043 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)) ∈ ℂ) |
| 37 | 27, 36 | mulcld 11281 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) ∈ ℂ) |
| 38 | 19, 37 | eqeltrrd 2842 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) ∈
ℂ) |
| 39 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑘 = ((2 · 𝑛) + 1) → (𝑘 − 1) = (((2 ·
𝑛) + 1) −
1)) |
| 40 | 39 | oveq1d 7446 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((𝑘 − 1) / 2) = ((((2
· 𝑛) + 1) − 1)
/ 2)) |
| 41 | 40 | oveq2d 7447 |
. . . . 5
⊢ (𝑘 = ((2 · 𝑛) + 1) → (-1↑((𝑘 − 1) / 2)) =
(-1↑((((2 · 𝑛)
+ 1) − 1) / 2))) |
| 42 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → (𝐴↑𝑘) = (𝐴↑((2 · 𝑛) + 1))) |
| 43 | | id 22 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → 𝑘 = ((2 · 𝑛) + 1)) |
| 44 | 42, 43 | oveq12d 7449 |
. . . . 5
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((𝐴↑𝑘) / 𝑘) = ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) |
| 45 | 41, 44 | oveq12d 7449 |
. . . 4
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((-1↑((𝑘 − 1) / 2)) ·
((𝐴↑𝑘) / 𝑘)) = ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
| 46 | 38, 45 | iserodd 16873 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (seq0( + , (𝑛 ∈
ℕ0 ↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝
(arctan‘𝐴) ↔
seq1( + , (𝑘 ∈ ℕ
↦ if(2 ∥ 𝑘, 0,
((-1↑((𝑘 − 1) /
2)) · ((𝐴↑𝑘) / 𝑘))))) ⇝ (arctan‘𝐴))) |
| 47 | 24, 46 | mpbird 257 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝
(arctan‘𝐴)) |
| 48 | 22, 47 | eqbrtrd 5165 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) ⇝
(arctan‘𝐴)) |