# Metamath Proof Explorer

## Theorem fta1

Description: The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg ( F ) roots. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis fta1.1 ${⊢}{R}={{F}}^{-1}\left[\left\{0\right\}\right]$
Assertion fta1 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fta1.1 ${⊢}{R}={{F}}^{-1}\left[\left\{0\right\}\right]$
2 eqid ${⊢}\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)$
3 dgrcl ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \mathrm{deg}\left({F}\right)\in {ℕ}_{0}$
4 3 adantr ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \mathrm{deg}\left({F}\right)\in {ℕ}_{0}$
5 eqeq2 ${⊢}{x}=0\to \left(\mathrm{deg}\left({f}\right)={x}↔\mathrm{deg}\left({f}\right)=0\right)$
6 5 imbi1d ${⊢}{x}=0\to \left(\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({f}\right)=0\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
7 6 ralbidv ${⊢}{x}=0\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=0\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
8 eqeq2 ${⊢}{x}={d}\to \left(\mathrm{deg}\left({f}\right)={x}↔\mathrm{deg}\left({f}\right)={d}\right)$
9 8 imbi1d ${⊢}{x}={d}\to \left(\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({f}\right)={d}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
10 9 ralbidv ${⊢}{x}={d}\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
11 eqeq2 ${⊢}{x}={d}+1\to \left(\mathrm{deg}\left({f}\right)={x}↔\mathrm{deg}\left({f}\right)={d}+1\right)$
12 11 imbi1d ${⊢}{x}={d}+1\to \left(\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({f}\right)={d}+1\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
13 12 ralbidv ${⊢}{x}={d}+1\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}+1\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
14 eqeq2 ${⊢}{x}=\mathrm{deg}\left({F}\right)\to \left(\mathrm{deg}\left({f}\right)={x}↔\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\right)$
15 14 imbi1d ${⊢}{x}=\mathrm{deg}\left({F}\right)\to \left(\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
16 15 ralbidv ${⊢}{x}=\mathrm{deg}\left({F}\right)\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={x}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
17 eldifsni ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to {f}\ne {0}_{𝑝}$
18 17 adantr ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to {f}\ne {0}_{𝑝}$
19 simplr ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to \mathrm{deg}\left({f}\right)=0$
20 eldifi ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to {f}\in \mathrm{Poly}\left(ℂ\right)$
21 20 ad2antrr ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}\in \mathrm{Poly}\left(ℂ\right)$
22 0dgrb ${⊢}{f}\in \mathrm{Poly}\left(ℂ\right)\to \left(\mathrm{deg}\left({f}\right)=0↔{f}=ℂ×\left\{{f}\left(0\right)\right\}\right)$
23 21 22 syl ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to \left(\mathrm{deg}\left({f}\right)=0↔{f}=ℂ×\left\{{f}\left(0\right)\right\}\right)$
24 19 23 mpbid ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}=ℂ×\left\{{f}\left(0\right)\right\}$
25 24 fveq1d ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}\left({x}\right)=\left(ℂ×\left\{{f}\left(0\right)\right\}\right)\left({x}\right)$
26 20 adantr ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to {f}\in \mathrm{Poly}\left(ℂ\right)$
27 plyf ${⊢}{f}\in \mathrm{Poly}\left(ℂ\right)\to {f}:ℂ⟶ℂ$
28 ffn ${⊢}{f}:ℂ⟶ℂ\to {f}Fnℂ$
29 fniniseg ${⊢}{f}Fnℂ\to \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]↔\left({x}\in ℂ\wedge {f}\left({x}\right)=0\right)\right)$
30 26 27 28 29 4syl ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]↔\left({x}\in ℂ\wedge {f}\left({x}\right)=0\right)\right)$
31 30 biimpa ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to \left({x}\in ℂ\wedge {f}\left({x}\right)=0\right)$
32 31 simprd ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}\left({x}\right)=0$
33 31 simpld ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {x}\in ℂ$
34 fvex ${⊢}{f}\left(0\right)\in \mathrm{V}$
35 34 fvconst2 ${⊢}{x}\in ℂ\to \left(ℂ×\left\{{f}\left(0\right)\right\}\right)\left({x}\right)={f}\left(0\right)$
36 33 35 syl ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to \left(ℂ×\left\{{f}\left(0\right)\right\}\right)\left({x}\right)={f}\left(0\right)$
37 25 32 36 3eqtr3rd ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}\left(0\right)=0$
38 37 sneqd ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to \left\{{f}\left(0\right)\right\}=\left\{0\right\}$
39 38 xpeq2d ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to ℂ×\left\{{f}\left(0\right)\right\}=ℂ×\left\{0\right\}$
40 24 39 eqtrd ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}=ℂ×\left\{0\right\}$
41 df-0p ${⊢}{0}_{𝑝}=ℂ×\left\{0\right\}$
42 40 41 syl6eqr ${⊢}\left(\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\wedge {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)\to {f}={0}_{𝑝}$
43 42 ex ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\to {f}={0}_{𝑝}\right)$
44 43 necon3ad ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to \left({f}\ne {0}_{𝑝}\to ¬{x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\right)$
45 18 44 mpd ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to ¬{x}\in {{f}}^{-1}\left[\left\{0\right\}\right]$
46 45 eq0rdv ${⊢}\left({f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \mathrm{deg}\left({f}\right)=0\right)\to {{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing$
47 46 ex ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to \left(\mathrm{deg}\left({f}\right)=0\to {{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \right)$
48 dgrcl ${⊢}{f}\in \mathrm{Poly}\left(ℂ\right)\to \mathrm{deg}\left({f}\right)\in {ℕ}_{0}$
49 nn0ge0 ${⊢}\mathrm{deg}\left({f}\right)\in {ℕ}_{0}\to 0\le \mathrm{deg}\left({f}\right)$
50 20 48 49 3syl ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to 0\le \mathrm{deg}\left({f}\right)$
51 id ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to {{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing$
52 0fin ${⊢}\varnothing \in \mathrm{Fin}$
53 51 52 syl6eqel ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to {{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}$
54 53 biantrurd ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left(\left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)↔\left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
55 fveq2 ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|=\left|\varnothing \right|$
56 hash0 ${⊢}\left|\varnothing \right|=0$
57 55 56 syl6eq ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|=0$
58 57 breq1d ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left(\left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)↔0\le \mathrm{deg}\left({f}\right)\right)$
59 54 58 bitr3d ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left(\left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)↔0\le \mathrm{deg}\left({f}\right)\right)$
60 50 59 syl5ibrcom ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
61 47 60 syld ${⊢}{f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to \left(\mathrm{deg}\left({f}\right)=0\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
62 61 rgen ${⊢}\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=0\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
63 fveqeq2 ${⊢}{f}={g}\to \left(\mathrm{deg}\left({f}\right)={d}↔\mathrm{deg}\left({g}\right)={d}\right)$
64 cnveq ${⊢}{f}={g}\to {{f}}^{-1}={{g}}^{-1}$
65 64 imaeq1d ${⊢}{f}={g}\to {{f}}^{-1}\left[\left\{0\right\}\right]={{g}}^{-1}\left[\left\{0\right\}\right]$
66 65 eleq1d ${⊢}{f}={g}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}↔{{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\right)$
67 65 fveq2d ${⊢}{f}={g}\to \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|=\left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|$
68 fveq2 ${⊢}{f}={g}\to \mathrm{deg}\left({f}\right)=\mathrm{deg}\left({g}\right)$
69 67 68 breq12d ${⊢}{f}={g}\to \left(\left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)↔\left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)$
70 66 69 anbi12d ${⊢}{f}={g}\to \left(\left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)↔\left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)$
71 63 70 imbi12d ${⊢}{f}={g}\to \left(\left(\mathrm{deg}\left({f}\right)={d}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)$
72 71 cbvralvw ${⊢}\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)$
73 50 ad2antlr ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to 0\le \mathrm{deg}\left({f}\right)$
74 73 59 syl5ibrcom ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
75 74 a1dd ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]=\varnothing \to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
76 n0 ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {{f}}^{-1}\left[\left\{0\right\}\right]$
77 eqid ${⊢}{{f}}^{-1}\left[\left\{0\right\}\right]={{f}}^{-1}\left[\left\{0\right\}\right]$
78 simplll ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to {d}\in {ℕ}_{0}$
79 simpllr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)$
80 simplr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to \mathrm{deg}\left({f}\right)={d}+1$
81 simprl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to {x}\in {{f}}^{-1}\left[\left\{0\right\}\right]$
82 simprr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)$
83 77 78 79 80 81 82 fta1lem ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\wedge \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\wedge \forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)$
84 83 exp32 ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left({x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
85 84 exlimdv ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {{f}}^{-1}\left[\left\{0\right\}\right]\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
86 76 85 syl5bi ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\ne \varnothing \to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
87 75 86 pm2.61dne ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\wedge \mathrm{deg}\left({f}\right)={d}+1\right)\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
88 87 ex ${⊢}\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\to \left(\mathrm{deg}\left({f}\right)={d}+1\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
89 88 com23 ${⊢}\left({d}\in {ℕ}_{0}\wedge {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\right)\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \left(\mathrm{deg}\left({f}\right)={d}+1\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
90 89 ralrimdva ${⊢}{d}\in {ℕ}_{0}\to \left(\forall {g}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({g}\right)={d}\to \left({{g}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{g}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({g}\right)\right)\right)\to \forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}+1\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
91 72 90 syl5bi ${⊢}{d}\in {ℕ}_{0}\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\to \forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)={d}+1\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\right)$
92 7 10 13 16 62 91 nn0ind ${⊢}\mathrm{deg}\left({F}\right)\in {ℕ}_{0}\to \forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
93 4 92 syl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)$
94 plyssc ${⊢}\mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left(ℂ\right)$
95 94 sseli ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}\in \mathrm{Poly}\left(ℂ\right)$
96 eldifsn ${⊢}{F}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)↔\left({F}\in \mathrm{Poly}\left(ℂ\right)\wedge {F}\ne {0}_{𝑝}\right)$
97 fveqeq2 ${⊢}{f}={F}\to \left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)↔\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\right)$
98 cnveq ${⊢}{f}={F}\to {{f}}^{-1}={{F}}^{-1}$
99 98 imaeq1d ${⊢}{f}={F}\to {{f}}^{-1}\left[\left\{0\right\}\right]={{F}}^{-1}\left[\left\{0\right\}\right]$
100 99 1 syl6eqr ${⊢}{f}={F}\to {{f}}^{-1}\left[\left\{0\right\}\right]={R}$
101 100 eleq1d ${⊢}{f}={F}\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}↔{R}\in \mathrm{Fin}\right)$
102 100 fveq2d ${⊢}{f}={F}\to \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|=\left|{R}\right|$
103 fveq2 ${⊢}{f}={F}\to \mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)$
104 102 103 breq12d ${⊢}{f}={F}\to \left(\left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)↔\left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)$
105 101 104 anbi12d ${⊢}{f}={F}\to \left(\left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)↔\left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)$
106 97 105 imbi12d ${⊢}{f}={F}\to \left(\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)↔\left(\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)\right)$
107 106 rspcv ${⊢}{F}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\to \left(\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)\right)$
108 96 107 sylbir ${⊢}\left({F}\in \mathrm{Poly}\left(ℂ\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\to \left(\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)\right)$
109 95 108 sylan ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left(\forall {f}\in \left(\mathrm{Poly}\left(ℂ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{deg}\left({f}\right)=\mathrm{deg}\left({F}\right)\to \left({{f}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{f}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({f}\right)\right)\right)\to \left(\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)\right)$
110 93 109 mpd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left(\mathrm{deg}\left({F}\right)=\mathrm{deg}\left({F}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)\right)$
111 2 110 mpi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left({R}\in \mathrm{Fin}\wedge \left|{R}\right|\le \mathrm{deg}\left({F}\right)\right)$