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 syl6eq ⊢ ( ( ◡ 𝑓 “ { 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 ‘ 𝐹 ) ) )