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 ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )

Proof

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