Step | Hyp | Ref
| Expression |
1 | | atantayl3.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
((-1↑𝑛) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
2 | | 2nn0 12131 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
3 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
4 | | nn0mulcl 12150 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
5 | 2, 3, 4 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (2 · 𝑛) ∈
ℕ0) |
6 | 5 | nn0cnd 12176 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (2 · 𝑛) ∈ ℂ) |
7 | | ax-1cn 10811 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
8 | | pncan 11108 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
9 | 6, 7, 8 | sylancl 589 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛)) |
10 | 9 | oveq1d 7246 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((((2 · 𝑛) + 1) − 1) / 2) = ((2 · 𝑛) / 2)) |
11 | | nn0cn 12124 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
12 | 11 | adantl 485 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 ∈ ℂ) |
13 | | 2cnd 11932 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 2 ∈ ℂ) |
14 | | 2ne0 11958 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
15 | 14 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 2 ≠ 0) |
16 | 12, 13, 15 | divcan3d 11637 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) / 2) = 𝑛) |
17 | 10, 16 | eqtr2d 2779 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 = ((((2 · 𝑛) + 1) − 1) / 2)) |
18 | 17 | oveq2d 7247 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (-1↑𝑛) = (-1↑((((2 · 𝑛) + 1) − 1) /
2))) |
19 | 18 | oveq1d 7246 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) = ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
20 | 19 | mpteq2dva 5164 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ0 ↦
((-1↑((((2 · 𝑛)
+ 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) |
21 | 1, 20 | syl5eq 2791 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐹 = (𝑛 ∈ ℕ0
↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) |
22 | 21 | seqeq3d 13606 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) = seq0(
+ , (𝑛 ∈
ℕ0 ↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))))) |
23 | | eqid 2738 |
. . . 4
⊢ (𝑘 ∈ ℕ ↦ if(2
∥ 𝑘, 0,
((-1↑((𝑘 − 1) /
2)) · ((𝐴↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) ·
((𝐴↑𝑘) / 𝑘)))) |
24 | 23 | atantayl2 25845 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑘 ∈
ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · ((𝐴↑𝑘) / 𝑘))))) ⇝ (arctan‘𝐴)) |
25 | | neg1cn 11968 |
. . . . . . 7
⊢ -1 ∈
ℂ |
26 | | expcl 13677 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ 𝑛
∈ ℕ0) → (-1↑𝑛) ∈ ℂ) |
27 | 25, 3, 26 | sylancr 590 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (-1↑𝑛) ∈ ℂ) |
28 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝐴 ∈ ℂ) |
29 | | peano2nn0 12154 |
. . . . . . . . 9
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈
ℕ0) |
30 | 5, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈
ℕ0) |
31 | 28, 30 | expcld 13740 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (𝐴↑((2 · 𝑛) + 1)) ∈ ℂ) |
32 | | nn0p1nn 12153 |
. . . . . . . . 9
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ) |
33 | 5, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ) |
34 | 33 | nncnd 11870 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈ ℂ) |
35 | 33 | nnne0d 11904 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ≠ 0) |
36 | 31, 34, 35 | divcld 11632 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)) ∈ ℂ) |
37 | 27, 36 | mulcld 10877 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) ∈ ℂ) |
38 | 19, 37 | eqeltrrd 2840 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) ∈
ℂ) |
39 | | oveq1 7238 |
. . . . . . 7
⊢ (𝑘 = ((2 · 𝑛) + 1) → (𝑘 − 1) = (((2 ·
𝑛) + 1) −
1)) |
40 | 39 | oveq1d 7246 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((𝑘 − 1) / 2) = ((((2
· 𝑛) + 1) − 1)
/ 2)) |
41 | 40 | oveq2d 7247 |
. . . . 5
⊢ (𝑘 = ((2 · 𝑛) + 1) → (-1↑((𝑘 − 1) / 2)) =
(-1↑((((2 · 𝑛)
+ 1) − 1) / 2))) |
42 | | oveq2 7239 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → (𝐴↑𝑘) = (𝐴↑((2 · 𝑛) + 1))) |
43 | | id 22 |
. . . . . 6
⊢ (𝑘 = ((2 · 𝑛) + 1) → 𝑘 = ((2 · 𝑛) + 1)) |
44 | 42, 43 | oveq12d 7249 |
. . . . 5
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((𝐴↑𝑘) / 𝑘) = ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))) |
45 | 41, 44 | oveq12d 7249 |
. . . 4
⊢ (𝑘 = ((2 · 𝑛) + 1) → ((-1↑((𝑘 − 1) / 2)) ·
((𝐴↑𝑘) / 𝑘)) = ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) ·
((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) |
46 | 38, 45 | iserodd 16412 |
. . 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 260 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((-1↑((((2 · 𝑛) + 1) − 1) / 2)) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))) ⇝
(arctan‘𝐴)) |
48 | 22, 47 | eqbrtrd 5089 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) ⇝
(arctan‘𝐴)) |