Proof of Theorem atantayl2
Step | Hyp | Ref
| Expression |
1 | | atantayl2.1 |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) ·
((𝐴↑𝑛) / 𝑛)))) |
2 | | ax-icn 9874 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
3 | 2 | negcli 10228 |
. . . . . . . . . . . . . . 15
⊢ -i ∈
ℂ |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → -i ∈
ℂ) |
5 | | nnnn0 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
6 | 5 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 𝑛 ∈
ℕ0) |
7 | 4, 6 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(-i↑𝑛) ∈
ℂ) |
8 | | sqneg 12785 |
. . . . . . . . . . . . . . . . 17
⊢ (i ∈
ℂ → (-i↑2) = (i↑2)) |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(-i↑2) = (i↑2) |
10 | 9 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢
((-i↑2)↑(𝑛
/ 2)) = ((i↑2)↑(𝑛
/ 2)) |
11 | | ine0 10344 |
. . . . . . . . . . . . . . . . . 18
⊢ i ≠
0 |
12 | 2, 11 | negne0i 10235 |
. . . . . . . . . . . . . . . . 17
⊢ -i ≠
0 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → -i ≠
0) |
14 | | 2z 11286 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 2 ∈
ℤ) |
16 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) → 2
∈ ℤ) |
17 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) → 2
≠ 0) |
19 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℤ) |
21 | | dvdsval2 14824 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ 𝑛 ∈ ℤ) → (2 ∥ 𝑛 ↔ (𝑛 / 2) ∈ ℤ)) |
22 | 16, 18, 20, 21 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) → (2
∥ 𝑛 ↔ (𝑛 / 2) ∈
ℤ)) |
23 | 22 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (𝑛 / 2) ∈
ℤ) |
24 | | expmulz 12768 |
. . . . . . . . . . . . . . . 16
⊢ (((-i
∈ ℂ ∧ -i ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑛 / 2) ∈ ℤ)) →
(-i↑(2 · (𝑛 /
2))) = ((-i↑2)↑(𝑛
/ 2))) |
25 | 4, 13, 15, 23, 24 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(-i↑(2 · (𝑛 /
2))) = ((-i↑2)↑(𝑛
/ 2))) |
26 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → i ∈
ℂ) |
27 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → i ≠
0) |
28 | | expmulz 12768 |
. . . . . . . . . . . . . . . 16
⊢ (((i
∈ ℂ ∧ i ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑛 / 2) ∈ ℤ)) →
(i↑(2 · (𝑛 /
2))) = ((i↑2)↑(𝑛
/ 2))) |
29 | 26, 27, 15, 23, 28 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(i↑(2 · (𝑛 /
2))) = ((i↑2)↑(𝑛
/ 2))) |
30 | 10, 25, 29 | 3eqtr4a 2670 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(-i↑(2 · (𝑛 /
2))) = (i↑(2 · (𝑛 / 2)))) |
31 | | nncn 10905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
32 | 31 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 𝑛 ∈
ℂ) |
33 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 2 ∈
ℂ) |
34 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 2 ≠
0) |
35 | 32, 33, 34 | divcan2d 10682 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (2
· (𝑛 / 2)) = 𝑛) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(-i↑(2 · (𝑛 /
2))) = (-i↑𝑛)) |
37 | 35 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(i↑(2 · (𝑛 /
2))) = (i↑𝑛)) |
38 | 30, 36, 37 | 3eqtr3d 2652 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
(-i↑𝑛) = (i↑𝑛)) |
39 | 7, 38 | subeq0bd 10335 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) →
((-i↑𝑛) −
(i↑𝑛)) =
0) |
40 | 39 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (i
· ((-i↑𝑛)
− (i↑𝑛))) = (i
· 0)) |
41 | | it0e0 11131 |
. . . . . . . . . . 11
⊢ (i
· 0) = 0 |
42 | 40, 41 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (i
· ((-i↑𝑛)
− (i↑𝑛))) =
0) |
43 | 42 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → ((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2) =
(0 / 2)) |
44 | | 2cn 10968 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
45 | 44, 17 | div0i 10638 |
. . . . . . . . 9
⊢ (0 / 2) =
0 |
46 | 43, 45 | syl6eq 2660 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → ((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2) =
0) |
47 | 46 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2)
· ((𝐴↑𝑛) / 𝑛)) = (0 · ((𝐴↑𝑛) / 𝑛))) |
48 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 𝐴 ∈
ℂ) |
49 | 48, 6 | expcld 12870 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (𝐴↑𝑛) ∈ ℂ) |
50 | | nnne0 10930 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
51 | 50 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 𝑛 ≠ 0) |
52 | 49, 32, 51 | divcld 10680 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → ((𝐴↑𝑛) / 𝑛) ∈ ℂ) |
53 | 52 | mul02d 10113 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → (0
· ((𝐴↑𝑛) / 𝑛)) = 0) |
54 | 47, 53 | eqtr2d 2645 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧ 2
∥ 𝑛) → 0 = (((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2)
· ((𝐴↑𝑛) / 𝑛))) |
55 | | 2cnd 10970 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → 2
∈ ℂ) |
56 | | ax-1cn 9873 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
57 | 56 | negcli 10228 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
58 | 57 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
-1 ∈ ℂ) |
59 | | neg1ne0 11003 |
. . . . . . . . . 10
⊢ -1 ≠
0 |
60 | 59 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
-1 ≠ 0) |
61 | 31 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
𝑛 ∈
ℂ) |
62 | | peano2cn 10087 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (𝑛 + 1) ∈
ℂ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(𝑛 + 1) ∈
ℂ) |
64 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → 2
≠ 0) |
65 | 63, 55, 55, 64 | divsubdird 10719 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(((𝑛 + 1) − 2) / 2) =
(((𝑛 + 1) / 2) − (2 /
2))) |
66 | | 2div2e1 11027 |
. . . . . . . . . . . . 13
⊢ (2 / 2) =
1 |
67 | 66 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ (((𝑛 + 1) / 2) − (2 / 2)) =
(((𝑛 + 1) / 2) −
1) |
68 | 65, 67 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(((𝑛 + 1) − 2) / 2) =
(((𝑛 + 1) / 2) −
1)) |
69 | | df-2 10956 |
. . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) |
70 | 69 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ ((𝑛 + 1) − 2) = ((𝑛 + 1) − (1 +
1)) |
71 | 56 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → 1
∈ ℂ) |
72 | 61, 71, 71 | pnpcan2d 10309 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((𝑛 + 1) − (1 + 1)) =
(𝑛 −
1)) |
73 | 70, 72 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((𝑛 + 1) − 2) =
(𝑛 −
1)) |
74 | 73 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(((𝑛 + 1) − 2) / 2) =
((𝑛 − 1) /
2)) |
75 | 68, 74 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(((𝑛 + 1) / 2) − 1) =
((𝑛 − 1) /
2)) |
76 | 22 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(¬ 2 ∥ 𝑛 ↔
¬ (𝑛 / 2) ∈
ℤ)) |
77 | | zeo 11339 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨
((𝑛 + 1) / 2) ∈
ℤ)) |
78 | 20, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
((𝑛 / 2) ∈ ℤ
∨ ((𝑛 + 1) / 2) ∈
ℤ)) |
79 | 78 | ord 391 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(¬ (𝑛 / 2) ∈
ℤ → ((𝑛 + 1) /
2) ∈ ℤ)) |
80 | 76, 79 | sylbid 229 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(¬ 2 ∥ 𝑛 →
((𝑛 + 1) / 2) ∈
ℤ)) |
81 | 80 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((𝑛 + 1) / 2) ∈
ℤ) |
82 | | peano2zm 11297 |
. . . . . . . . . . 11
⊢ (((𝑛 + 1) / 2) ∈ ℤ →
(((𝑛 + 1) / 2) − 1)
∈ ℤ) |
83 | 81, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(((𝑛 + 1) / 2) − 1)
∈ ℤ) |
84 | 75, 83 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((𝑛 − 1) / 2) ∈
ℤ) |
85 | 58, 60, 84 | expclzd 12875 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-1↑((𝑛 − 1) /
2)) ∈ ℂ) |
86 | 85 | 2timesd 11152 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(2 · (-1↑((𝑛
− 1) / 2))) = ((-1↑((𝑛 − 1) / 2)) + (-1↑((𝑛 − 1) /
2)))) |
87 | | subcl 10159 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
1) ∈ ℂ) |
88 | 61, 56, 87 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(𝑛 − 1) ∈
ℂ) |
89 | 88, 55, 64 | divcan2d 10682 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(2 · ((𝑛 − 1)
/ 2)) = (𝑛 −
1)) |
90 | 89 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i↑(2 · ((𝑛
− 1) / 2))) = (-i↑(𝑛 − 1))) |
91 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
-i ∈ ℂ) |
92 | 12 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
-i ≠ 0) |
93 | 19 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
𝑛 ∈
ℤ) |
94 | 91, 92, 93 | expm1d 12880 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i↑(𝑛 − 1)) =
((-i↑𝑛) /
-i)) |
95 | 90, 94 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i↑(2 · ((𝑛
− 1) / 2))) = ((-i↑𝑛) / -i)) |
96 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → 2
∈ ℤ) |
97 | | expmulz 12768 |
. . . . . . . . . . . . 13
⊢ (((-i
∈ ℂ ∧ -i ≠ 0) ∧ (2 ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈
ℤ)) → (-i↑(2 · ((𝑛 − 1) / 2))) =
((-i↑2)↑((𝑛
− 1) / 2))) |
98 | 91, 92, 96, 84, 97 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i↑(2 · ((𝑛
− 1) / 2))) = ((-i↑2)↑((𝑛 − 1) / 2))) |
99 | 5 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
𝑛 ∈
ℕ0) |
100 | | expcl 12740 |
. . . . . . . . . . . . . 14
⊢ ((-i
∈ ℂ ∧ 𝑛
∈ ℕ0) → (-i↑𝑛) ∈ ℂ) |
101 | 3, 99, 100 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i↑𝑛) ∈
ℂ) |
102 | 101, 91, 92 | divrec2d 10684 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((-i↑𝑛) / -i) = ((1 /
-i) · (-i↑𝑛))) |
103 | 95, 98, 102 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((-i↑2)↑((𝑛
− 1) / 2)) = ((1 / -i) · (-i↑𝑛))) |
104 | | i2 12827 |
. . . . . . . . . . . . 13
⊢
(i↑2) = -1 |
105 | 9, 104 | eqtri 2632 |
. . . . . . . . . . . 12
⊢
(-i↑2) = -1 |
106 | 105 | oveq1i 6559 |
. . . . . . . . . . 11
⊢
((-i↑2)↑((𝑛 − 1) / 2)) = (-1↑((𝑛 − 1) /
2)) |
107 | | irec 12826 |
. . . . . . . . . . . . . 14
⊢ (1 / i) =
-i |
108 | 107 | negeqi 10153 |
. . . . . . . . . . . . 13
⊢ -(1 / i)
= --i |
109 | | divneg2 10628 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → -(1 / i) = (1 /
-i)) |
110 | 56, 2, 11, 109 | mp3an 1416 |
. . . . . . . . . . . . 13
⊢ -(1 / i)
= (1 / -i) |
111 | 2 | negnegi 10230 |
. . . . . . . . . . . . 13
⊢ --i =
i |
112 | 108, 110,
111 | 3eqtr3i 2640 |
. . . . . . . . . . . 12
⊢ (1 / -i)
= i |
113 | 112 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ ((1 / -i)
· (-i↑𝑛)) = (i
· (-i↑𝑛)) |
114 | 103, 106,
113 | 3eqtr3g 2667 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-1↑((𝑛 − 1) /
2)) = (i · (-i↑𝑛))) |
115 | 89 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i↑(2 · ((𝑛
− 1) / 2))) = (i↑(𝑛 − 1))) |
116 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → i
∈ ℂ) |
117 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) → i
≠ 0) |
118 | 116, 117,
93 | expm1d 12880 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i↑(𝑛 − 1)) =
((i↑𝑛) /
i)) |
119 | 115, 118 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i↑(2 · ((𝑛
− 1) / 2))) = ((i↑𝑛) / i)) |
120 | | expmulz 12768 |
. . . . . . . . . . . . . 14
⊢ (((i
∈ ℂ ∧ i ≠ 0) ∧ (2 ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈
ℤ)) → (i↑(2 · ((𝑛 − 1) / 2))) = ((i↑2)↑((𝑛 − 1) /
2))) |
121 | 116, 117,
96, 84, 120 | syl22anc 1319 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i↑(2 · ((𝑛
− 1) / 2))) = ((i↑2)↑((𝑛 − 1) / 2))) |
122 | | expcl 12740 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ 𝑛
∈ ℕ0) → (i↑𝑛) ∈ ℂ) |
123 | 2, 99, 122 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i↑𝑛) ∈
ℂ) |
124 | 123, 116,
117 | divrec2d 10684 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((i↑𝑛) / i) = ((1 / i)
· (i↑𝑛))) |
125 | 119, 121,
124 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((i↑2)↑((𝑛
− 1) / 2)) = ((1 / i) · (i↑𝑛))) |
126 | 104 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢
((i↑2)↑((𝑛
− 1) / 2)) = (-1↑((𝑛 − 1) / 2)) |
127 | 107 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ ((1 / i)
· (i↑𝑛)) = (-i
· (i↑𝑛)) |
128 | 125, 126,
127 | 3eqtr3g 2667 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-1↑((𝑛 − 1) /
2)) = (-i · (i↑𝑛))) |
129 | | mulneg1 10345 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (i↑𝑛) ∈ ℂ) → (-i ·
(i↑𝑛)) = -(i ·
(i↑𝑛))) |
130 | 2, 123, 129 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-i · (i↑𝑛)) =
-(i · (i↑𝑛))) |
131 | 128, 130 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-1↑((𝑛 − 1) /
2)) = -(i · (i↑𝑛))) |
132 | 114, 131 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((-1↑((𝑛 − 1) /
2)) + (-1↑((𝑛 −
1) / 2))) = ((i · (-i↑𝑛)) + -(i · (i↑𝑛)))) |
133 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (-i↑𝑛) ∈ ℂ) → (i ·
(-i↑𝑛)) ∈
ℂ) |
134 | 2, 101, 133 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i · (-i↑𝑛))
∈ ℂ) |
135 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (i↑𝑛) ∈ ℂ) → (i ·
(i↑𝑛)) ∈
ℂ) |
136 | 2, 123, 135 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i · (i↑𝑛))
∈ ℂ) |
137 | 134, 136 | negsubd 10277 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((i · (-i↑𝑛)) +
-(i · (i↑𝑛))) =
((i · (-i↑𝑛))
− (i · (i↑𝑛)))) |
138 | 116, 101,
123 | subdid 10365 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(i · ((-i↑𝑛)
− (i↑𝑛))) = ((i
· (-i↑𝑛))
− (i · (i↑𝑛)))) |
139 | 137, 138 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((i · (-i↑𝑛)) +
-(i · (i↑𝑛))) =
(i · ((-i↑𝑛)
− (i↑𝑛)))) |
140 | 86, 132, 139 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(2 · (-1↑((𝑛
− 1) / 2))) = (i · ((-i↑𝑛) − (i↑𝑛)))) |
141 | 55, 85, 64, 140 | mvllmuld 10736 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
(-1↑((𝑛 − 1) /
2)) = ((i · ((-i↑𝑛) − (i↑𝑛))) / 2)) |
142 | 141 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) ∧
¬ 2 ∥ 𝑛) →
((-1↑((𝑛 − 1) /
2)) · ((𝐴↑𝑛) / 𝑛)) = (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))) |
143 | 54, 142 | ifeqda 4071 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
if(2 ∥ 𝑛, 0,
((-1↑((𝑛 − 1) /
2)) · ((𝐴↑𝑛) / 𝑛))) = (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))) |
144 | 143 | mpteq2dva 4672 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝑛 ∈ ℕ
↦ if(2 ∥ 𝑛, 0,
((-1↑((𝑛 − 1) /
2)) · ((𝐴↑𝑛) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((i ·
((-i↑𝑛) −
(i↑𝑛))) / 2) ·
((𝐴↑𝑛) / 𝑛)))) |
145 | 1, 144 | syl5eq 2656 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐹 = (𝑛 ∈ ℕ ↦ (((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2)
· ((𝐴↑𝑛) / 𝑛)))) |
146 | 145 | seqeq3d 12671 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , 𝐹) = seq1(
+ , (𝑛 ∈ ℕ
↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))))) |
147 | | eqid 2610 |
. . 3
⊢ (𝑛 ∈ ℕ ↦ (((i
· ((-i↑𝑛)
− (i↑𝑛))) / 2)
· ((𝐴↑𝑛) / 𝑛))) = (𝑛 ∈ ℕ ↦ (((i ·
((-i↑𝑛) −
(i↑𝑛))) / 2) ·
((𝐴↑𝑛) / 𝑛))) |
148 | 147 | atantayl 24464 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑛 ∈
ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛)))) ⇝ (arctan‘𝐴)) |
149 | 146, 148 | eqbrtrd 4605 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , 𝐹) ⇝
(arctan‘𝐴)) |