Step |
Hyp |
Ref |
Expression |
1 |
|
aasscn |
⊢ 𝔸 ⊆ ℂ |
2 |
|
eldifi |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ∈ 𝔸 ) |
3 |
1 2
|
sseldi |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ∈ ℂ ) |
4 |
|
elaa |
⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 ) ) |
5 |
2 4
|
sylib |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 ) ) |
6 |
5
|
simprd |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 ) |
7 |
2
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝔸 ) |
8 |
|
eldifsni |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ≠ 0 ) |
9 |
8
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝐴 ≠ 0 ) |
10 |
|
eldifi |
⊢ ( 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑔 ∈ ( Poly ‘ ℤ ) ) |
11 |
10
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝑔 ∈ ( Poly ‘ ℤ ) ) |
12 |
|
eldifsni |
⊢ ( 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑔 ≠ 0𝑝 ) |
13 |
12
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝑔 ≠ 0𝑝 ) |
14 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → ( 𝑔 ‘ 𝐴 ) = 0 ) |
15 |
|
fveq2 |
⊢ ( 𝑚 = 𝑛 → ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) = ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ) |
16 |
15
|
neeq1d |
⊢ ( 𝑚 = 𝑛 → ( ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 ) ) |
17 |
16
|
cbvrabv |
⊢ { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } = { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 } |
18 |
17
|
infeq1i |
⊢ inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) |
19 |
|
fvoveq1 |
⊢ ( 𝑗 = 𝑘 → ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) = ( ( coeff ‘ 𝑔 ) ‘ ( 𝑘 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) |
20 |
19
|
cbvmptv |
⊢ ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑘 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) |
21 |
|
eqid |
⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝑔 ) − inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ( ( ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝑔 ) − inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ( ( ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
22 |
7 9 11 13 14 18 20 21
|
elaa2lem |
⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
23 |
22
|
rexlimdv3a |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ) |
24 |
6 23
|
mpd |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
25 |
3 24
|
jca |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ) |
26 |
|
simpl |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → 𝑓 ∈ ( Poly ‘ ℤ ) ) |
27 |
|
fveq2 |
⊢ ( 𝑓 = 0𝑝 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 0𝑝 ) ) |
28 |
|
coe0 |
⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } ) |
29 |
27 28
|
eqtrdi |
⊢ ( 𝑓 = 0𝑝 → ( coeff ‘ 𝑓 ) = ( ℕ0 × { 0 } ) ) |
30 |
29
|
fveq1d |
⊢ ( 𝑓 = 0𝑝 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = ( ( ℕ0 × { 0 } ) ‘ 0 ) ) |
31 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
32 |
|
fvconst2g |
⊢ ( ( 0 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0 ) |
33 |
31 31 32
|
mp2an |
⊢ ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0 |
34 |
30 33
|
eqtrdi |
⊢ ( 𝑓 = 0𝑝 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 ) |
35 |
34
|
adantl |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝑓 = 0𝑝 ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 ) |
36 |
|
neneq |
⊢ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 → ¬ ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 ) |
37 |
36
|
ad2antlr |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝑓 = 0𝑝 ) → ¬ ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 ) |
38 |
35 37
|
pm2.65da |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → ¬ 𝑓 = 0𝑝 ) |
39 |
|
velsn |
⊢ ( 𝑓 ∈ { 0𝑝 } ↔ 𝑓 = 0𝑝 ) |
40 |
38 39
|
sylnibr |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → ¬ 𝑓 ∈ { 0𝑝 } ) |
41 |
26 40
|
eldifd |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) |
42 |
41
|
adantrr |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) |
43 |
|
simprr |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ‘ 𝐴 ) = 0 ) |
44 |
42 43
|
jca |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
45 |
44
|
reximi2 |
⊢ ( ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) |
46 |
45
|
anim2i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
47 |
|
elaa |
⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
48 |
46 47
|
sylibr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝔸 ) |
49 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
50 |
|
nfv |
⊢ Ⅎ 𝑓 𝐴 ∈ ℂ |
51 |
|
nfre1 |
⊢ Ⅎ 𝑓 ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) |
52 |
50 51
|
nfan |
⊢ Ⅎ 𝑓 ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
53 |
|
nfv |
⊢ Ⅎ 𝑓 ¬ 𝐴 ∈ { 0 } |
54 |
|
simpl3r |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = 0 ) |
55 |
|
fveq2 |
⊢ ( 𝐴 = 0 → ( 𝑓 ‘ 𝐴 ) = ( 𝑓 ‘ 0 ) ) |
56 |
|
eqid |
⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 ) |
57 |
56
|
coefv0 |
⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( 𝑓 ‘ 0 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) |
58 |
55 57
|
sylan9eqr |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) |
59 |
58
|
adantlr |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) |
60 |
|
simplr |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) |
61 |
59 60
|
eqnetrd |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) ≠ 0 ) |
62 |
61
|
neneqd |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 ) |
63 |
62
|
adantlrr |
⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 ) |
64 |
63
|
3adantl1 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 ) |
65 |
54 64
|
pm2.65da |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 = 0 ) |
66 |
|
elsng |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 ) ) |
67 |
66
|
biimpa |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ { 0 } ) → 𝐴 = 0 ) |
68 |
67
|
3ad2antl1 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 ∈ { 0 } ) → 𝐴 = 0 ) |
69 |
65 68
|
mtand |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 ∈ { 0 } ) |
70 |
69
|
3exp |
⊢ ( 𝐴 ∈ ℂ → ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) ) ) |
71 |
70
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) ) ) |
72 |
52 53 71
|
rexlimd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) ) |
73 |
49 72
|
mpd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 ∈ { 0 } ) |
74 |
48 73
|
eldifd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ) |
75 |
25 74
|
impbii |
⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ) |