Proof of Theorem atandm2
| Step | Hyp | Ref
| Expression |
| 1 | | atandm 26919 |
. 2
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) |
| 2 | | 3anass 1095 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0) ↔ (𝐴 ∈
ℂ ∧ ((1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))) |
| 3 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 4 | | ax-icn 11214 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
| 5 | | mulcl 11239 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 6 | 4, 5 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
| 7 | | subeq0 11535 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → ((1 − (i
· 𝐴)) = 0 ↔ 1 =
(i · 𝐴))) |
| 8 | 3, 6, 7 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((1
− (i · 𝐴)) = 0
↔ 1 = (i · 𝐴))) |
| 9 | 4, 4 | mulneg2i 11710 |
. . . . . . . . . . . 12
⊢ (i
· -i) = -(i · i) |
| 10 | | ixi 11892 |
. . . . . . . . . . . . 13
⊢ (i
· i) = -1 |
| 11 | 10 | negeqi 11501 |
. . . . . . . . . . . 12
⊢ -(i
· i) = --1 |
| 12 | | negneg1e1 12384 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
| 13 | 9, 11, 12 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ (i
· -i) = 1 |
| 14 | 13 | eqeq2i 2750 |
. . . . . . . . . 10
⊢ ((i
· 𝐴) = (i ·
-i) ↔ (i · 𝐴) =
1) |
| 15 | | eqcom 2744 |
. . . . . . . . . 10
⊢ ((i
· 𝐴) = 1 ↔ 1 =
(i · 𝐴)) |
| 16 | 14, 15 | bitri 275 |
. . . . . . . . 9
⊢ ((i
· 𝐴) = (i ·
-i) ↔ 1 = (i · 𝐴)) |
| 17 | 8, 16 | bitr4di 289 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((1
− (i · 𝐴)) = 0
↔ (i · 𝐴) = (i
· -i))) |
| 18 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
| 19 | 4 | negcli 11577 |
. . . . . . . . . 10
⊢ -i ∈
ℂ |
| 20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → -i ∈
ℂ) |
| 21 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) |
| 22 | | ine0 11698 |
. . . . . . . . . 10
⊢ i ≠
0 |
| 23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → i ≠
0) |
| 24 | 18, 20, 21, 23 | mulcand 11896 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· 𝐴) = (i ·
-i) ↔ 𝐴 =
-i)) |
| 25 | 17, 24 | bitrd 279 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1
− (i · 𝐴)) = 0
↔ 𝐴 =
-i)) |
| 26 | 25 | necon3bid 2985 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((1
− (i · 𝐴))
≠ 0 ↔ 𝐴 ≠
-i)) |
| 27 | | addcom 11447 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) = ((i · 𝐴) + 1)) |
| 28 | 3, 6, 27 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (1 + (i
· 𝐴)) = ((i ·
𝐴) + 1)) |
| 29 | | subneg 11558 |
. . . . . . . . . . . . 13
⊢ (((i
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → ((i · 𝐴) − -1) = ((i · 𝐴) + 1)) |
| 30 | 6, 3, 29 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· 𝐴) − -1) =
((i · 𝐴) +
1)) |
| 31 | 28, 30 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (1 + (i
· 𝐴)) = ((i ·
𝐴) −
-1)) |
| 32 | 31 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → ((1 + (i
· 𝐴)) = 0 ↔ ((i
· 𝐴) − -1) =
0)) |
| 33 | 3 | negcli 11577 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
| 34 | | subeq0 11535 |
. . . . . . . . . . 11
⊢ (((i
· 𝐴) ∈ ℂ
∧ -1 ∈ ℂ) → (((i · 𝐴) − -1) = 0 ↔ (i · 𝐴) = -1)) |
| 35 | 6, 33, 34 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (((i
· 𝐴) − -1) = 0
↔ (i · 𝐴) =
-1)) |
| 36 | 32, 35 | bitrd 279 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((1 + (i
· 𝐴)) = 0 ↔ (i
· 𝐴) =
-1)) |
| 37 | 10 | eqeq2i 2750 |
. . . . . . . . 9
⊢ ((i
· 𝐴) = (i ·
i) ↔ (i · 𝐴) =
-1) |
| 38 | 36, 37 | bitr4di 289 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((1 + (i
· 𝐴)) = 0 ↔ (i
· 𝐴) = (i ·
i))) |
| 39 | 18, 21, 21, 23 | mulcand 11896 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· 𝐴) = (i ·
i) ↔ 𝐴 =
i)) |
| 40 | 38, 39 | bitrd 279 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1 + (i
· 𝐴)) = 0 ↔
𝐴 = i)) |
| 41 | 40 | necon3bid 2985 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((1 + (i
· 𝐴)) ≠ 0 ↔
𝐴 ≠ i)) |
| 42 | 26, 41 | anbi12d 632 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (((1
− (i · 𝐴))
≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0) ↔ (𝐴 ≠ -i ∧ 𝐴 ≠ i))) |
| 43 | 42 | pm5.32i 574 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ ((1
− (i · 𝐴))
≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) ↔ (𝐴 ∈ ℂ ∧ (𝐴 ≠ -i ∧ 𝐴 ≠ i))) |
| 44 | | 3anass 1095 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i) ↔ (𝐴 ∈ ℂ ∧ (𝐴 ≠ -i ∧ 𝐴 ≠ i))) |
| 45 | 43, 44 | bitr4i 278 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ((1
− (i · 𝐴))
≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) |
| 46 | 2, 45 | bitri 275 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0) ↔ (𝐴 ∈
ℂ ∧ 𝐴 ≠ -i
∧ 𝐴 ≠
i)) |
| 47 | 1, 46 | bitr4i 278 |
1
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |