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