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-10
Assertion fta1 ⊢F∈Poly⁡S∧F≠0𝑝→R∈Fin∧R≤deg⁡F

Proof

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