Metamath Proof Explorer


Theorem atandmcj

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

Ref Expression
Assertion atandmcj ( 𝐴 ∈ dom arctan → ( ∗ ‘ 𝐴 ) ∈ dom arctan )

Proof

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