Metamath Proof Explorer

Theorem atandmcj

Description: The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandmcj ⊢ A ∈ dom ⁡ arctan → A ‾ ∈ dom ⁡ arctan

Proof

Step Hyp Ref Expression
1 atandm3 ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A 2 ≠ − 1
2 1 simplbi ⊢ A ∈ dom ⁡ arctan → A ∈ ℂ
3 2 cjcld ⊢ A ∈ dom ⁡ arctan → A ‾ ∈ ℂ
4 2nn0 ⊢ 2 ∈ ℕ 0
5 cjexp ⊢ A ∈ ℂ ∧ 2 ∈ ℕ 0 → A 2 ‾ = A ‾ 2
6 2 4 5 sylancl ⊢ A ∈ dom ⁡ arctan → A 2 ‾ = A ‾ 2
7 2 sqcld ⊢ A ∈ dom ⁡ arctan → A 2 ∈ ℂ
8 7 cjcjd ⊢ A ∈ dom ⁡ arctan → A 2 ‾ ‾ = A 2
9 1 simprbi ⊢ A ∈ dom ⁡ arctan → A 2 ≠ − 1
10 8 9 eqnetrd ⊢ A ∈ dom ⁡ arctan → A 2 ‾ ‾ ≠ − 1
11 fveq2 ⊢ A 2 ‾ = − 1 → A 2 ‾ ‾ = − 1 ‾
12 neg1rr ⊢ − 1 ∈ ℝ
13 cjre ⊢ − 1 ∈ ℝ → − 1 ‾ = − 1
14 12 13 ax-mp ⊢ − 1 ‾ = − 1
15 11 14 eqtrdi ⊢ A 2 ‾ = − 1 → A 2 ‾ ‾ = − 1
16 15 necon3i ⊢ A 2 ‾ ‾ ≠ − 1 → A 2 ‾ ≠ − 1
17 10 16 syl ⊢ A ∈ dom ⁡ arctan → A 2 ‾ ≠ − 1
18 6 17 eqnetrrd ⊢ A ∈ dom ⁡ arctan → A ‾ 2 ≠ − 1
19 atandm3 ⊢ A ‾ ∈ dom ⁡ arctan ↔ A ‾ ∈ ℂ ∧ A ‾ 2 ≠ − 1
20 3 18 19 sylanbrc ⊢ A ∈ dom ⁡ arctan → A ‾ ∈ dom ⁡ arctan