Proof of Theorem aannenlem1
Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. . . . . . 7
deg deg |
2 | | breq2 4657 |
. . . . . . . 8
coeff coeff |
3 | 2 | ralbidv 2986 |
. . . . . . 7
coeff coeff |
4 | 1, 3 | 3anbi23d 1402 |
. . . . . 6
deg
coeff deg coeff |
5 | 4 | rabbidv 3189 |
. . . . 5
Poly
deg coeff Poly
deg
coeff |
6 | 5 | rexeqdv 3145 |
. . . 4
Poly
deg coeff Poly
deg
coeff |
7 | 6 | rabbidv 3189 |
. . 3
Poly deg coeff
Poly
deg coeff |
8 | | aannenlem.a |
. . 3
Poly
deg
coeff |
9 | | cnex 10017 |
. . . 4
|
10 | 9 | rabex 4813 |
. . 3
Poly deg coeff |
11 | 7, 8, 10 | fvmpt 6282 |
. 2
Poly
deg
coeff |
12 | | iunrab 4567 |
. . 3
Poly deg
coeff Poly
deg
coeff |
13 | | fzfi 12771 |
. . . . . . 7
|
14 | | fzfi 12771 |
. . . . . . 7
|
15 | | mapfi 8262 |
. . . . . . 7
|
16 | 13, 14, 15 | mp2an 708 |
. . . . . 6
|
17 | 16 | a1i 11 |
. . . . 5
|
18 | | ovex 6678 |
. . . . . 6
|
19 | | neeq1 2856 |
. . . . . . . . . . 11
|
20 | | fveq2 6191 |
. . . . . . . . . . . 12
deg deg |
21 | 20 | breq1d 4663 |
. . . . . . . . . . 11
deg deg |
22 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
coeff coeff |
23 | 22 | fveq1d 6193 |
. . . . . . . . . . . . . 14
coeff coeff |
24 | 23 | fveq2d 6195 |
. . . . . . . . . . . . 13
coeff coeff |
25 | 24 | breq1d 4663 |
. . . . . . . . . . . 12
coeff coeff |
26 | 25 | ralbidv 2986 |
. . . . . . . . . . 11
coeff coeff |
27 | 19, 21, 26 | 3anbi123d 1399 |
. . . . . . . . . 10
deg
coeff deg coeff |
28 | 27 | elrab 3363 |
. . . . . . . . 9
Poly deg coeff
Poly deg
coeff |
29 | | simp3 1063 |
. . . . . . . . . 10
deg
coeff
coeff |
30 | 29 | anim2i 593 |
. . . . . . . . 9
Poly
deg
coeff Poly
coeff |
31 | 28, 30 | sylbi 207 |
. . . . . . . 8
Poly deg coeff Poly
coeff |
32 | | 0z 11388 |
. . . . . . . . . . . . . . 15
|
33 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
coeff coeff |
34 | 33 | coef2 23987 |
. . . . . . . . . . . . . . 15
Poly
coeff |
35 | 32, 34 | mpan2 707 |
. . . . . . . . . . . . . 14
Poly coeff |
36 | 35 | ad2antrl 764 |
. . . . . . . . . . . . 13
Poly
coeff
coeff |
37 | 36 | ffnd 6046 |
. . . . . . . . . . . 12
Poly
coeff
coeff |
38 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Poly coeff |
39 | 38 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
Poly coeff |
40 | 39 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
Poly coeff |
41 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
Poly |
43 | 40, 42 | absled 14169 |
. . . . . . . . . . . . . . . . 17
Poly coeff coeff coeff |
44 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | 44 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
Poly |
46 | 45 | znegcld 11484 |
. . . . . . . . . . . . . . . . . 18
Poly |
47 | | elfz 12332 |
. . . . . . . . . . . . . . . . . 18
coeff coeff
coeff coeff |
48 | 39, 46, 45, 47 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
Poly coeff
coeff coeff |
49 | 43, 48 | bitr4d 271 |
. . . . . . . . . . . . . . . 16
Poly coeff coeff |
50 | 49 | biimpd 219 |
. . . . . . . . . . . . . . 15
Poly coeff coeff |
51 | 50 | ralimdva 2962 |
. . . . . . . . . . . . . 14
Poly
coeff coeff |
52 | 51 | impr 649 |
. . . . . . . . . . . . 13
Poly
coeff
coeff |
53 | | fnfvrnss 6390 |
. . . . . . . . . . . . 13
coeff coeff
coeff
|
54 | 37, 52, 53 | syl2anc 693 |
. . . . . . . . . . . 12
Poly
coeff
coeff |
55 | | df-f 5892 |
. . . . . . . . . . . 12
coeff coeff coeff |
56 | 37, 54, 55 | sylanbrc 698 |
. . . . . . . . . . 11
Poly
coeff
coeff |
57 | | fz0ssnn0 12435 |
. . . . . . . . . . 11
|
58 | | fssres 6070 |
. . . . . . . . . . 11
coeff
coeff |
59 | 56, 57, 58 | sylancl 694 |
. . . . . . . . . 10
Poly
coeff
coeff |
60 | | ovex 6678 |
. . . . . . . . . . 11
|
61 | | ovex 6678 |
. . . . . . . . . . 11
|
62 | 60, 61 | elmap 7886 |
. . . . . . . . . 10
coeff coeff |
63 | 59, 62 | sylibr 224 |
. . . . . . . . 9
Poly
coeff
coeff |
64 | 63 | ex 450 |
. . . . . . . 8
Poly
coeff coeff |
65 | 31, 64 | syl5 34 |
. . . . . . 7
Poly deg coeff coeff |
66 | | simp2 1062 |
. . . . . . . . . 10
deg
coeff
deg
|
67 | 66 | anim2i 593 |
. . . . . . . . 9
Poly
deg
coeff Poly
deg |
68 | 28, 67 | sylbi 207 |
. . . . . . . 8
Poly deg coeff Poly
deg |
69 | | neeq1 2856 |
. . . . . . . . . . 11
|
70 | | fveq2 6191 |
. . . . . . . . . . . 12
deg deg |
71 | 70 | breq1d 4663 |
. . . . . . . . . . 11
deg deg |
72 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
coeff coeff |
73 | 72 | fveq1d 6193 |
. . . . . . . . . . . . . 14
coeff coeff |
74 | 73 | fveq2d 6195 |
. . . . . . . . . . . . 13
coeff coeff |
75 | 74 | breq1d 4663 |
. . . . . . . . . . . 12
coeff coeff |
76 | 75 | ralbidv 2986 |
. . . . . . . . . . 11
coeff coeff |
77 | 69, 71, 76 | 3anbi123d 1399 |
. . . . . . . . . 10
deg
coeff deg coeff |
78 | 77 | elrab 3363 |
. . . . . . . . 9
Poly deg coeff
Poly deg
coeff |
79 | | simp2 1062 |
. . . . . . . . . 10
deg
coeff
deg
|
80 | 79 | anim2i 593 |
. . . . . . . . 9
Poly
deg
coeff Poly
deg |
81 | 78, 80 | sylbi 207 |
. . . . . . . 8
Poly deg coeff Poly
deg |
82 | | simplll 798 |
. . . . . . . . . . . . 13
Poly deg Poly
deg
coeff coeff Poly |
83 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly |
84 | | ffn 6045 |
. . . . . . . . . . . . 13
|
85 | 82, 83, 84 | 3syl 18 |
. . . . . . . . . . . 12
Poly deg Poly
deg
coeff coeff |
86 | | simplrl 800 |
. . . . . . . . . . . . 13
Poly deg Poly
deg
coeff coeff Poly |
87 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly |
88 | | ffn 6045 |
. . . . . . . . . . . . 13
|
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . 12
Poly deg Poly
deg
coeff coeff |
90 | | simplrr 801 |
. . . . . . . . . . . . . . . . . 18
Poly deg
Poly deg
coeff coeff coeff coeff |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Poly
deg
Poly deg
coeff coeff coeff coeff |
92 | 91 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
Poly
deg
Poly deg
coeff coeff coeff coeff |
93 | | fvres 6207 |
. . . . . . . . . . . . . . . . 17
coeff coeff |
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . . 16
Poly
deg
Poly deg
coeff coeff coeff coeff |
95 | | fvres 6207 |
. . . . . . . . . . . . . . . . 17
coeff coeff |
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . 16
Poly
deg
Poly deg
coeff coeff coeff coeff |
97 | 92, 94, 96 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
Poly
deg
Poly deg
coeff coeff coeff coeff |
98 | 97 | oveq1d 6665 |
. . . . . . . . . . . . . 14
Poly
deg
Poly deg
coeff coeff coeff coeff |
99 | 98 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
Poly deg
Poly deg
coeff coeff coeff coeff |
100 | | simp-4l 806 |
. . . . . . . . . . . . . 14
Poly deg
Poly deg
coeff coeff Poly |
101 | | simp-4r 807 |
. . . . . . . . . . . . . . 15
Poly deg
Poly deg
coeff coeff deg
|
102 | | dgrcl 23989 |
. . . . . . . . . . . . . . . . 17
Poly deg |
103 | | nn0z 11400 |
. . . . . . . . . . . . . . . . 17
deg deg |
104 | 100, 102,
103 | 3syl 18 |
. . . . . . . . . . . . . . . 16
Poly deg
Poly deg
coeff coeff deg |
105 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
Poly deg
Poly deg
coeff coeff |
106 | 105 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
Poly deg
Poly deg
coeff coeff |
107 | | eluz 11701 |
. . . . . . . . . . . . . . . 16
deg
deg deg |
108 | 104, 106,
107 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Poly deg
Poly deg
coeff coeff deg
deg
|
109 | 101, 108 | mpbird 247 |
. . . . . . . . . . . . . 14
Poly deg
Poly deg
coeff coeff deg |
110 | | simpr 477 |
. . . . . . . . . . . . . 14
Poly deg
Poly deg
coeff coeff |
111 | | eqid 2622 |
. . . . . . . . . . . . . . 15
deg deg |
112 | 33, 111 | coeid3 23996 |
. . . . . . . . . . . . . 14
Poly
deg coeff |
113 | 100, 109,
110, 112 | syl3anc 1326 |
. . . . . . . . . . . . 13
Poly deg
Poly deg
coeff coeff
coeff |
114 | | simp1rl 1126 |
. . . . . . . . . . . . . . 15
Poly deg Poly
deg
coeff coeff
Poly |
115 | 114 | 3expa 1265 |
. . . . . . . . . . . . . 14
Poly deg
Poly deg
coeff coeff Poly |
116 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
Poly deg Poly
deg
coeff coeff deg
|
117 | 116 | adantr 481 |
. . . . . . . . . . . . . . 15
Poly deg
Poly deg
coeff coeff deg
|
118 | | dgrcl 23989 |
. . . . . . . . . . . . . . . . 17
Poly deg |
119 | | nn0z 11400 |
. . . . . . . . . . . . . . . . 17
deg deg |
120 | 115, 118,
119 | 3syl 18 |
. . . . . . . . . . . . . . . 16
Poly deg
Poly deg
coeff coeff deg |
121 | | eluz 11701 |
. . . . . . . . . . . . . . . 16
deg
deg deg |
122 | 120, 106,
121 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Poly deg
Poly deg
coeff coeff deg
deg
|
123 | 117, 122 | mpbird 247 |
. . . . . . . . . . . . . 14
Poly deg
Poly deg
coeff coeff deg |
124 | | eqid 2622 |
. . . . . . . . . . . . . . 15
coeff coeff |
125 | | eqid 2622 |
. . . . . . . . . . . . . . 15
deg deg |
126 | 124, 125 | coeid3 23996 |
. . . . . . . . . . . . . 14
Poly
deg coeff |
127 | 115, 123,
110, 126 | syl3anc 1326 |
. . . . . . . . . . . . 13
Poly deg
Poly deg
coeff coeff
coeff |
128 | 99, 113, 127 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
Poly deg
Poly deg
coeff coeff |
129 | 85, 89, 128 | eqfnfvd 6314 |
. . . . . . . . . . 11
Poly deg Poly
deg
coeff coeff |
130 | 129 | expr 643 |
. . . . . . . . . 10
Poly deg Poly
deg coeff coeff |
131 | | fveq2 6191 |
. . . . . . . . . . 11
coeff coeff |
132 | 131 | reseq1d 5395 |
. . . . . . . . . 10
coeff coeff |
133 | 130, 132 | impbid1 215 |
. . . . . . . . 9
Poly deg Poly
deg coeff coeff
|
134 | 133 | expcom 451 |
. . . . . . . 8
Poly deg
Poly deg coeff coeff |
135 | 68, 81, 134 | syl2ani 688 |
. . . . . . 7
Poly
deg coeff Poly deg
coeff coeff coeff |
136 | 65, 135 | dom2d 7996 |
. . . . . 6
Poly
deg coeff
|
137 | 18, 136 | mpi 20 |
. . . . 5
Poly
deg coeff
|
138 | | domfi 8181 |
. . . . 5
Poly
deg
coeff
Poly deg coeff |
139 | 17, 137, 138 | syl2anc 693 |
. . . 4
Poly
deg coeff |
140 | | neeq1 2856 |
. . . . . . . . 9
|
141 | | fveq2 6191 |
. . . . . . . . . 10
deg deg |
142 | 141 | breq1d 4663 |
. . . . . . . . 9
deg deg |
143 | | fveq2 6191 |
. . . . . . . . . . . . 13
coeff coeff |
144 | 143 | fveq1d 6193 |
. . . . . . . . . . . 12
coeff coeff |
145 | 144 | fveq2d 6195 |
. . . . . . . . . . 11
coeff coeff |
146 | 145 | breq1d 4663 |
. . . . . . . . . 10
coeff coeff |
147 | 146 | ralbidv 2986 |
. . . . . . . . 9
coeff coeff |
148 | 140, 142,
147 | 3anbi123d 1399 |
. . . . . . . 8
deg
coeff deg coeff |
149 | 148 | elrab 3363 |
. . . . . . 7
Poly deg coeff
Poly deg
coeff |
150 | | simp1 1061 |
. . . . . . . 8
deg
coeff
|
151 | 150 | anim2i 593 |
. . . . . . 7
Poly
deg
coeff Poly
|
152 | 149, 151 | sylbi 207 |
. . . . . 6
Poly deg coeff Poly
|
153 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly |
154 | 153 | ffnd 6046 |
. . . . . . . . . . . 12
Poly |
155 | 154 | adantr 481 |
. . . . . . . . . . 11
Poly
|
156 | | fniniseg 6338 |
. . . . . . . . . . 11
|
157 | 155, 156 | syl 17 |
. . . . . . . . . 10
Poly
|
158 | | fveq2 6191 |
. . . . . . . . . . . 12
|
159 | 158 | eqeq1d 2624 |
. . . . . . . . . . 11
|
160 | 159 | elrab 3363 |
. . . . . . . . . 10
|
161 | 157, 160 | syl6rbbr 279 |
. . . . . . . . 9
Poly
|
162 | 161 | eqrdv 2620 |
. . . . . . . 8
Poly
|
163 | | eqid 2622 |
. . . . . . . . . 10
|
164 | 163 | fta1 24063 |
. . . . . . . . 9
Poly
deg |
165 | 164 | simpld 475 |
. . . . . . . 8
Poly
|
166 | 162, 165 | eqeltrd 2701 |
. . . . . . 7
Poly
|
167 | 166 | a1i 11 |
. . . . . 6
Poly
|
168 | 152, 167 | syl5 34 |
. . . . 5
Poly deg coeff |
169 | 168 | ralrimiv 2965 |
. . . 4
Poly deg
coeff |
170 | | iunfi 8254 |
. . . 4
Poly deg
coeff Poly
deg
coeff
Poly deg
coeff |
171 | 139, 169,
170 | syl2anc 693 |
. . 3
Poly deg
coeff |
172 | 12, 171 | syl5eqelr 2706 |
. 2
Poly deg coeff |
173 | 11, 172 | eqeltrd 2701 |
1
|