Step |
Hyp |
Ref |
Expression |
1 |
|
cjcl |
⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ ) |
3 |
|
fveq2 |
⊢ ( ( 𝑓 ‘ 𝐴 ) = 0 → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = ( ∗ ‘ 0 ) ) |
4 |
|
cj0 |
⊢ ( ∗ ‘ 0 ) = 0 |
5 |
3 4
|
eqtrdi |
⊢ ( ( 𝑓 ‘ 𝐴 ) = 0 → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = 0 ) |
6 |
|
difss |
⊢ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ⊆ ( Poly ‘ ℤ ) |
7 |
|
zssre |
⊢ ℤ ⊆ ℝ |
8 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
9 |
|
plyss |
⊢ ( ( ℤ ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) ) |
10 |
7 8 9
|
mp2an |
⊢ ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) |
11 |
6 10
|
sstri |
⊢ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ⊆ ( Poly ‘ ℝ ) |
12 |
11
|
sseli |
⊢ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑓 ∈ ( Poly ‘ ℝ ) ) |
13 |
|
id |
⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ ) |
14 |
|
plyrecj |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) ) |
15 |
12 13 14
|
syl2anr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) ) |
16 |
15
|
eqeq1d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = 0 ↔ ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) ) |
17 |
5 16
|
syl5ib |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ( 𝑓 ‘ 𝐴 ) = 0 → ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) ) |
18 |
17
|
reximdva |
⊢ ( 𝐴 ∈ ℂ → ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) ) |
19 |
18
|
imp |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) |
20 |
2 19
|
jca |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) → ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) ) |
21 |
|
elaa |
⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
22 |
|
elaa |
⊢ ( ( ∗ ‘ 𝐴 ) ∈ 𝔸 ↔ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) ) |
23 |
20 21 22
|
3imtr4i |
⊢ ( 𝐴 ∈ 𝔸 → ( ∗ ‘ 𝐴 ) ∈ 𝔸 ) |