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 )