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 ) |