Metamath Proof Explorer

Theorem atandm2

Description: This form of atandm is a bit more useful for showing that the logarithms in df-atan are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm2 ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0

Proof

Step Hyp Ref Expression
1 atandm ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
2 3anass ⊢ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0 ↔ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0
3 ax-1cn ⊢ 1 ∈ ℂ
4 ax-icn ⊢ i ∈ ℂ
5 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
6 4 5 mpan ⊢ A ∈ ℂ → i ⁢ A ∈ ℂ
7 subeq0 ⊢ 1 ∈ ℂ ∧ i ⁢ A ∈ ℂ → 1 − i ⁢ A = 0 ↔ 1 = i ⁢ A
8 3 6 7 sylancr ⊢ A ∈ ℂ → 1 − i ⁢ A = 0 ↔ 1 = i ⁢ A
9 4 4 mulneg2i ⊢ i ⁢ − i = − i ⁢ i
10 ixi ⊢ i ⁢ i = − 1
11 10 negeqi ⊢ − i ⁢ i = − -1
12 negneg1e1 ⊢ − -1 = 1
13 9 11 12 3eqtri ⊢ i ⁢ − i = 1
14 13 eqeq2i ⊢ i ⁢ A = i ⁢ − i ↔ i ⁢ A = 1
15 eqcom ⊢ i ⁢ A = 1 ↔ 1 = i ⁢ A
16 14 15 bitri ⊢ i ⁢ A = i ⁢ − i ↔ 1 = i ⁢ A
17 8 16 bitr4di ⊢ A ∈ ℂ → 1 − i ⁢ A = 0 ↔ i ⁢ A = i ⁢ − i
18 id ⊢ A ∈ ℂ → A ∈ ℂ
19 4 negcli ⊢ − i ∈ ℂ
20 19 a1i ⊢ A ∈ ℂ → − i ∈ ℂ
21 4 a1i ⊢ A ∈ ℂ → i ∈ ℂ
22 ine0 ⊢ i ≠ 0
23 22 a1i ⊢ A ∈ ℂ → i ≠ 0
24 18 20 21 23 mulcand ⊢ A ∈ ℂ → i ⁢ A = i ⁢ − i ↔ A = − i
25 17 24 bitrd ⊢ A ∈ ℂ → 1 − i ⁢ A = 0 ↔ A = − i
26 25 necon3bid ⊢ A ∈ ℂ → 1 − i ⁢ A ≠ 0 ↔ A ≠ − i
27 addcom ⊢ 1 ∈ ℂ ∧ i ⁢ A ∈ ℂ → 1 + i ⁢ A = i ⁢ A + 1
28 3 6 27 sylancr ⊢ A ∈ ℂ → 1 + i ⁢ A = i ⁢ A + 1
29 subneg ⊢ i ⁢ A ∈ ℂ ∧ 1 ∈ ℂ → i ⁢ A − -1 = i ⁢ A + 1
30 6 3 29 sylancl ⊢ A ∈ ℂ → i ⁢ A − -1 = i ⁢ A + 1
31 28 30 eqtr4d ⊢ A ∈ ℂ → 1 + i ⁢ A = i ⁢ A − -1
32 31 eqeq1d ⊢ A ∈ ℂ → 1 + i ⁢ A = 0 ↔ i ⁢ A − -1 = 0
33 3 negcli ⊢ − 1 ∈ ℂ
34 subeq0 ⊢ i ⁢ A ∈ ℂ ∧ − 1 ∈ ℂ → i ⁢ A − -1 = 0 ↔ i ⁢ A = − 1
35 6 33 34 sylancl ⊢ A ∈ ℂ → i ⁢ A − -1 = 0 ↔ i ⁢ A = − 1
36 32 35 bitrd ⊢ A ∈ ℂ → 1 + i ⁢ A = 0 ↔ i ⁢ A = − 1
37 10 eqeq2i ⊢ i ⁢ A = i ⁢ i ↔ i ⁢ A = − 1
38 36 37 bitr4di ⊢ A ∈ ℂ → 1 + i ⁢ A = 0 ↔ i ⁢ A = i ⁢ i
39 18 21 21 23 mulcand ⊢ A ∈ ℂ → i ⁢ A = i ⁢ i ↔ A = i
40 38 39 bitrd ⊢ A ∈ ℂ → 1 + i ⁢ A = 0 ↔ A = i
41 40 necon3bid ⊢ A ∈ ℂ → 1 + i ⁢ A ≠ 0 ↔ A ≠ i
42 26 41 anbi12d ⊢ A ∈ ℂ → 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0 ↔ A ≠ − i ∧ A ≠ i
43 42 pm5.32i ⊢ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0 ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
44 3anass ⊢ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
45 43 44 bitr4i ⊢ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0 ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
46 2 45 bitri ⊢ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0 ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
47 1 46 bitr4i ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ 1 − i ⁢ A ≠ 0 ∧ 1 + i ⁢ A ≠ 0