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 0
Assertion fta1 F Poly S F 0 𝑝 R Fin R deg F

Proof

Step Hyp Ref Expression
1 fta1.1 R = F -1 0
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 -1 0 Fin f -1 0 deg f deg f = 0 f -1 0 Fin f -1 0 deg f
7 6 ralbidv x = 0 f Poly 0 𝑝 deg f = x f -1 0 Fin f -1 0 deg f f Poly 0 𝑝 deg f = 0 f -1 0 Fin f -1 0 deg f
8 eqeq2 x = d deg f = x deg f = d
9 8 imbi1d x = d deg f = x f -1 0 Fin f -1 0 deg f deg f = d f -1 0 Fin f -1 0 deg f
10 9 ralbidv x = d f Poly 0 𝑝 deg f = x f -1 0 Fin f -1 0 deg f f Poly 0 𝑝 deg f = d f -1 0 Fin f -1 0 deg f
11 eqeq2 x = d + 1 deg f = x deg f = d + 1
12 11 imbi1d x = d + 1 deg f = x f -1 0 Fin f -1 0 deg f deg f = d + 1 f -1 0 Fin f -1 0 deg f
13 12 ralbidv x = d + 1 f Poly 0 𝑝 deg f = x f -1 0 Fin f -1 0 deg f f Poly 0 𝑝 deg f = d + 1 f -1 0 Fin f -1 0 deg f
14 eqeq2 x = deg F deg f = x deg f = deg F
15 14 imbi1d x = deg F deg f = x f -1 0 Fin f -1 0 deg f deg f = deg F f -1 0 Fin f -1 0 deg f
16 15 ralbidv x = deg F f Poly 0 𝑝 deg f = x f -1 0 Fin f -1 0 deg f f Poly 0 𝑝 deg f = deg F f -1 0 Fin f -1 0 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 -1 0 deg f = 0
20 eldifi f Poly 0 𝑝 f Poly
21 20 ad2antrr f Poly 0 𝑝 deg f = 0 x f -1 0 f Poly
22 0dgrb f Poly deg f = 0 f = × f 0
23 21 22 syl f Poly 0 𝑝 deg f = 0 x f -1 0 deg f = 0 f = × f 0
24 19 23 mpbid f Poly 0 𝑝 deg f = 0 x f -1 0 f = × f 0
25 24 fveq1d f Poly 0 𝑝 deg f = 0 x f -1 0 f x = × f 0 x
26 20 adantr f Poly 0 𝑝 deg f = 0 f Poly
27 plyf f Poly f :
28 ffn f : f Fn
29 fniniseg f Fn x f -1 0 x f x = 0
30 26 27 28 29 4syl f Poly 0 𝑝 deg f = 0 x f -1 0 x f x = 0
31 30 biimpa f Poly 0 𝑝 deg f = 0 x f -1 0 x f x = 0
32 31 simprd f Poly 0 𝑝 deg f = 0 x f -1 0 f x = 0
33 31 simpld f Poly 0 𝑝 deg f = 0 x f -1 0 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 -1 0 × f 0 x = f 0
37 25 32 36 3eqtr3rd f Poly 0 𝑝 deg f = 0 x f -1 0 f 0 = 0
38 37 sneqd f Poly 0 𝑝 deg f = 0 x f -1 0 f 0 = 0
39 38 xpeq2d f Poly 0 𝑝 deg f = 0 x f -1 0 × f 0 = × 0
40 24 39 eqtrd f Poly 0 𝑝 deg f = 0 x f -1 0 f = × 0
41 df-0p 0 𝑝 = × 0
42 40 41 eqtr4di f Poly 0 𝑝 deg f = 0 x f -1 0 f = 0 𝑝
43 42 ex f Poly 0 𝑝 deg f = 0 x f -1 0 f = 0 𝑝
44 43 necon3ad f Poly 0 𝑝 deg f = 0 f 0 𝑝 ¬ x f -1 0
45 18 44 mpd f Poly 0 𝑝 deg f = 0 ¬ x f -1 0
46 45 eq0rdv f Poly 0 𝑝 deg f = 0 f -1 0 =
47 46 ex f Poly 0 𝑝 deg f = 0 f -1 0 =
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 -1 0 = f -1 0 =
52 0fin Fin
53 51 52 eqeltrdi f -1 0 = f -1 0 Fin
54 53 biantrurd f -1 0 = f -1 0 deg f f -1 0 Fin f -1 0 deg f
55 fveq2 f -1 0 = f -1 0 =
56 hash0 = 0
57 55 56 eqtrdi f -1 0 = f -1 0 = 0
58 57 breq1d f -1 0 = f -1 0 deg f 0 deg f
59 54 58 bitr3d f -1 0 = f -1 0 Fin f -1 0 deg f 0 deg f
60 50 59 syl5ibrcom f Poly 0 𝑝 f -1 0 = f -1 0 Fin f -1 0 deg f
61 47 60 syld f Poly 0 𝑝 deg f = 0 f -1 0 Fin f -1 0 deg f
62 61 rgen f Poly 0 𝑝 deg f = 0 f -1 0 Fin f -1 0 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 -1 0 = g -1 0
66 65 eleq1d f = g f -1 0 Fin g -1 0 Fin
67 65 fveq2d f = g f -1 0 = g -1 0
68 fveq2 f = g deg f = deg g
69 67 68 breq12d f = g f -1 0 deg f g -1 0 deg g
70 66 69 anbi12d f = g f -1 0 Fin f -1 0 deg f g -1 0 Fin g -1 0 deg g
71 63 70 imbi12d f = g deg f = d f -1 0 Fin f -1 0 deg f deg g = d g -1 0 Fin g -1 0 deg g
72 71 cbvralvw f Poly 0 𝑝 deg f = d f -1 0 Fin f -1 0 deg f g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 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 -1 0 = f -1 0 Fin f -1 0 deg f
75 74 a1dd d 0 f Poly 0 𝑝 deg f = d + 1 f -1 0 = g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
76 n0 f -1 0 x x f -1 0
77 eqid f -1 0 = f -1 0
78 simplll d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g d 0
79 simpllr d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f Poly 0 𝑝
80 simplr d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g deg f = d + 1
81 simprl d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g x f -1 0
82 simprr d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g
83 77 78 79 80 81 82 fta1lem d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
84 83 exp32 d 0 f Poly 0 𝑝 deg f = d + 1 x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
85 84 exlimdv d 0 f Poly 0 𝑝 deg f = d + 1 x x f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
86 76 85 syl5bi d 0 f Poly 0 𝑝 deg f = d + 1 f -1 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
87 75 86 pm2.61dne d 0 f Poly 0 𝑝 deg f = d + 1 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
88 87 ex d 0 f Poly 0 𝑝 deg f = d + 1 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f -1 0 Fin f -1 0 deg f
89 88 com23 d 0 f Poly 0 𝑝 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g deg f = d + 1 f -1 0 Fin f -1 0 deg f
90 89 ralrimdva d 0 g Poly 0 𝑝 deg g = d g -1 0 Fin g -1 0 deg g f Poly 0 𝑝 deg f = d + 1 f -1 0 Fin f -1 0 deg f
91 72 90 syl5bi d 0 f Poly 0 𝑝 deg f = d f -1 0 Fin f -1 0 deg f f Poly 0 𝑝 deg f = d + 1 f -1 0 Fin f -1 0 deg f
92 7 10 13 16 62 91 nn0ind deg F 0 f Poly 0 𝑝 deg f = deg F f -1 0 Fin f -1 0 deg f
93 4 92 syl F Poly S F 0 𝑝 f Poly 0 𝑝 deg f = deg F f -1 0 Fin f -1 0 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 -1 0 = F -1 0
100 99 1 eqtr4di f = F f -1 0 = R
101 100 eleq1d f = F f -1 0 Fin R Fin
102 100 fveq2d f = F f -1 0 = R
103 fveq2 f = F deg f = deg F
104 102 103 breq12d f = F f -1 0 deg f R deg F
105 101 104 anbi12d f = F f -1 0 Fin f -1 0 deg f R Fin R deg F
106 97 105 imbi12d f = F deg f = deg F f -1 0 Fin f -1 0 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 -1 0 Fin f -1 0 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 -1 0 Fin f -1 0 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 -1 0 Fin f -1 0 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