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 𝑅 = ( 𝐹 “ { 0 } )
Assertion fta1 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fta1.1 𝑅 = ( 𝐹 “ { 0 } )
2 eqid ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
3 dgrcl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
4 3 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
5 eqeq2 ( 𝑥 = 0 → ( ( deg ‘ 𝑓 ) = 𝑥 ↔ ( deg ‘ 𝑓 ) = 0 ) )
6 5 imbi1d ( 𝑥 = 0 → ( ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝑓 ) = 0 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
7 6 ralbidv ( 𝑥 = 0 → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 0 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
8 eqeq2 ( 𝑥 = 𝑑 → ( ( deg ‘ 𝑓 ) = 𝑥 ↔ ( deg ‘ 𝑓 ) = 𝑑 ) )
9 8 imbi1d ( 𝑥 = 𝑑 → ( ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝑓 ) = 𝑑 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
10 9 ralbidv ( 𝑥 = 𝑑 → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑑 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
11 eqeq2 ( 𝑥 = ( 𝑑 + 1 ) → ( ( deg ‘ 𝑓 ) = 𝑥 ↔ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) )
12 11 imbi1d ( 𝑥 = ( 𝑑 + 1 ) → ( ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
13 12 ralbidv ( 𝑥 = ( 𝑑 + 1 ) → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
14 eqeq2 ( 𝑥 = ( deg ‘ 𝐹 ) → ( ( deg ‘ 𝑓 ) = 𝑥 ↔ ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) ) )
15 14 imbi1d ( 𝑥 = ( deg ‘ 𝐹 ) → ( ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
16 15 ralbidv ( 𝑥 = ( deg ‘ 𝐹 ) → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑥 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
17 eldifsni ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → 𝑓 ≠ 0𝑝 )
18 17 adantr ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → 𝑓 ≠ 0𝑝 )
19 simplr ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( deg ‘ 𝑓 ) = 0 )
20 eldifi ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → 𝑓 ∈ ( Poly ‘ ℂ ) )
21 20 ad2antrr ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → 𝑓 ∈ ( Poly ‘ ℂ ) )
22 0dgrb ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ 𝑓 ) = 0 ↔ 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) ) )
23 21 22 syl ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( ( deg ‘ 𝑓 ) = 0 ↔ 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) ) )
24 19 23 mpbid ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → 𝑓 = ( ℂ × { ( 𝑓 ‘ 0 ) } ) )
25 24 fveq1d ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( 𝑓𝑥 ) = ( ( ℂ × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑥 ) )
26 20 adantr ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → 𝑓 ∈ ( Poly ‘ ℂ ) )
27 plyf ( 𝑓 ∈ ( Poly ‘ ℂ ) → 𝑓 : ℂ ⟶ ℂ )
28 ffn ( 𝑓 : ℂ ⟶ ℂ → 𝑓 Fn ℂ )
29 fniniseg ( 𝑓 Fn ℂ → ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑓𝑥 ) = 0 ) ) )
30 26 27 28 29 4syl ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑓𝑥 ) = 0 ) ) )
31 30 biimpa ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( 𝑥 ∈ ℂ ∧ ( 𝑓𝑥 ) = 0 ) )
32 31 simprd ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( 𝑓𝑥 ) = 0 )
33 31 simpld ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → 𝑥 ∈ ℂ )
34 fvex ( 𝑓 ‘ 0 ) ∈ V
35 34 fvconst2 ( 𝑥 ∈ ℂ → ( ( ℂ × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑥 ) = ( 𝑓 ‘ 0 ) )
36 33 35 syl ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( ( ℂ × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑥 ) = ( 𝑓 ‘ 0 ) )
37 25 32 36 3eqtr3rd ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( 𝑓 ‘ 0 ) = 0 )
38 37 sneqd ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → { ( 𝑓 ‘ 0 ) } = { 0 } )
39 38 xpeq2d ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → ( ℂ × { ( 𝑓 ‘ 0 ) } ) = ( ℂ × { 0 } ) )
40 24 39 eqtrd ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → 𝑓 = ( ℂ × { 0 } ) )
41 df-0p 0𝑝 = ( ℂ × { 0 } )
42 40 41 eqtr4di ( ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) → 𝑓 = 0𝑝 )
43 42 ex ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → ( 𝑥 ∈ ( 𝑓 “ { 0 } ) → 𝑓 = 0𝑝 ) )
44 43 necon3ad ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → ( 𝑓 ≠ 0𝑝 → ¬ 𝑥 ∈ ( 𝑓 “ { 0 } ) ) )
45 18 44 mpd ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → ¬ 𝑥 ∈ ( 𝑓 “ { 0 } ) )
46 45 eq0rdv ( ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ∧ ( deg ‘ 𝑓 ) = 0 ) → ( 𝑓 “ { 0 } ) = ∅ )
47 46 ex ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → ( ( deg ‘ 𝑓 ) = 0 → ( 𝑓 “ { 0 } ) = ∅ ) )
48 dgrcl ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
49 nn0ge0 ( ( deg ‘ 𝑓 ) ∈ ℕ0 → 0 ≤ ( deg ‘ 𝑓 ) )
50 20 48 49 3syl ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → 0 ≤ ( deg ‘ 𝑓 ) )
51 id ( ( 𝑓 “ { 0 } ) = ∅ → ( 𝑓 “ { 0 } ) = ∅ )
52 0fin ∅ ∈ Fin
53 51 52 eqeltrdi ( ( 𝑓 “ { 0 } ) = ∅ → ( 𝑓 “ { 0 } ) ∈ Fin )
54 53 biantrurd ( ( 𝑓 “ { 0 } ) = ∅ → ( ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ↔ ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
55 fveq2 ( ( 𝑓 “ { 0 } ) = ∅ → ( ♯ ‘ ( 𝑓 “ { 0 } ) ) = ( ♯ ‘ ∅ ) )
56 hash0 ( ♯ ‘ ∅ ) = 0
57 55 56 eqtrdi ( ( 𝑓 “ { 0 } ) = ∅ → ( ♯ ‘ ( 𝑓 “ { 0 } ) ) = 0 )
58 57 breq1d ( ( 𝑓 “ { 0 } ) = ∅ → ( ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ↔ 0 ≤ ( deg ‘ 𝑓 ) ) )
59 54 58 bitr3d ( ( 𝑓 “ { 0 } ) = ∅ → ( ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ↔ 0 ≤ ( deg ‘ 𝑓 ) ) )
60 50 59 syl5ibrcom ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → ( ( 𝑓 “ { 0 } ) = ∅ → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
61 47 60 syld ( 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → ( ( deg ‘ 𝑓 ) = 0 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
62 61 rgen 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 0 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) )
63 fveqeq2 ( 𝑓 = 𝑔 → ( ( deg ‘ 𝑓 ) = 𝑑 ↔ ( deg ‘ 𝑔 ) = 𝑑 ) )
64 cnveq ( 𝑓 = 𝑔 𝑓 = 𝑔 )
65 64 imaeq1d ( 𝑓 = 𝑔 → ( 𝑓 “ { 0 } ) = ( 𝑔 “ { 0 } ) )
66 65 eleq1d ( 𝑓 = 𝑔 → ( ( 𝑓 “ { 0 } ) ∈ Fin ↔ ( 𝑔 “ { 0 } ) ∈ Fin ) )
67 65 fveq2d ( 𝑓 = 𝑔 → ( ♯ ‘ ( 𝑓 “ { 0 } ) ) = ( ♯ ‘ ( 𝑔 “ { 0 } ) ) )
68 fveq2 ( 𝑓 = 𝑔 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝑔 ) )
69 67 68 breq12d ( 𝑓 = 𝑔 → ( ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ↔ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) )
70 66 69 anbi12d ( 𝑓 = 𝑔 → ( ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ↔ ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
71 63 70 imbi12d ( 𝑓 = 𝑔 → ( ( ( deg ‘ 𝑓 ) = 𝑑 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) )
72 71 cbvralvw ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑑 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
73 50 ad2antlr ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → 0 ≤ ( deg ‘ 𝑓 ) )
74 73 59 syl5ibrcom ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( ( 𝑓 “ { 0 } ) = ∅ → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
75 74 a1dd ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( ( 𝑓 “ { 0 } ) = ∅ → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
76 n0 ( ( 𝑓 “ { 0 } ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑓 “ { 0 } ) )
77 eqid ( 𝑓 “ { 0 } ) = ( 𝑓 “ { 0 } )
78 simplll ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → 𝑑 ∈ ℕ0 )
79 simpllr ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
80 simplr ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) )
81 simprl ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → 𝑥 ∈ ( 𝑓 “ { 0 } ) )
82 simprr ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
83 77 78 79 80 81 82 fta1lem ( ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) ∧ ( 𝑥 ∈ ( 𝑓 “ { 0 } ) ∧ ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) )
84 83 exp32 ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( 𝑥 ∈ ( 𝑓 “ { 0 } ) → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
85 84 exlimdv ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( ∃ 𝑥 𝑥 ∈ ( 𝑓 “ { 0 } ) → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
86 76 85 syl5bi ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( ( 𝑓 “ { 0 } ) ≠ ∅ → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
87 75 86 pm2.61dne ( ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) ∧ ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) ) → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
88 87 ex ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) → ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
89 88 com23 ( ( 𝑑 ∈ ℕ0𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
90 89 ralrimdva ( 𝑑 ∈ ℕ0 → ( ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝑑 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) → ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
91 72 90 syl5bi ( 𝑑 ∈ ℕ0 → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = 𝑑 → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) → ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( 𝑑 + 1 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ) )
92 7 10 13 16 62 91 nn0ind ( ( deg ‘ 𝐹 ) ∈ ℕ0 → ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
93 4 92 syl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) )
94 plyssc ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
95 94 sseli ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
96 eldifsn ( 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) )
97 fveqeq2 ( 𝑓 = 𝐹 → ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) ↔ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) ) )
98 cnveq ( 𝑓 = 𝐹 𝑓 = 𝐹 )
99 98 imaeq1d ( 𝑓 = 𝐹 → ( 𝑓 “ { 0 } ) = ( 𝐹 “ { 0 } ) )
100 99 1 eqtr4di ( 𝑓 = 𝐹 → ( 𝑓 “ { 0 } ) = 𝑅 )
101 100 eleq1d ( 𝑓 = 𝐹 → ( ( 𝑓 “ { 0 } ) ∈ Fin ↔ 𝑅 ∈ Fin ) )
102 100 fveq2d ( 𝑓 = 𝐹 → ( ♯ ‘ ( 𝑓 “ { 0 } ) ) = ( ♯ ‘ 𝑅 ) )
103 fveq2 ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) )
104 102 103 breq12d ( 𝑓 = 𝐹 → ( ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ↔ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )
105 101 104 anbi12d ( 𝑓 = 𝐹 → ( ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ↔ ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) )
106 97 105 imbi12d ( 𝑓 = 𝐹 → ( ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) ↔ ( ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) ) )
107 106 rspcv ( 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) → ( ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) ) )
108 96 107 sylbir ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) → ( ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) ) )
109 95 108 sylan ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( ∀ 𝑓 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) → ( ( 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) ) → ( ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) ) )
110 93 109 mpd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) ) )
111 2 110 mpi ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )