Step | Hyp | Ref
| Expression |
1 | | elfznn0 12433 |
. . 3
deg
|
2 | | elqaa.6 |
. . . . 5
deg |
3 | 2 | fveq2i 6194 |
. . . 4
deg |
4 | | nnmulcl 11043 |
. . . . . 6
|
5 | 4 | adantl 482 |
. . . . 5
|
6 | | elfznn0 12433 |
. . . . . 6
deg
|
7 | | elqaa.1 |
. . . . . . . . 9
|
8 | | elqaa.2 |
. . . . . . . . 9
Poly |
9 | | elqaa.3 |
. . . . . . . . 9
|
10 | | elqaa.4 |
. . . . . . . . 9
coeff |
11 | | elqaa.5 |
. . . . . . . . 9
inf
|
12 | 7, 8, 9, 10, 11, 2 | elqaalem1 24074 |
. . . . . . . 8
|
13 | 12 | simpld 475 |
. . . . . . 7
|
14 | 13 | adantlr 751 |
. . . . . 6
|
15 | 6, 14 | sylan2 491 |
. . . . 5
deg |
16 | | eldifi 3732 |
. . . . . . . 8
Poly
Poly |
17 | | dgrcl 23989 |
. . . . . . . 8
Poly deg |
18 | 8, 16, 17 | 3syl 18 |
. . . . . . 7
deg |
19 | | nn0uz 11722 |
. . . . . . 7
|
20 | 18, 19 | syl6eleq 2711 |
. . . . . 6
deg |
21 | 20 | adantr 481 |
. . . . 5
deg |
22 | | nnz 11399 |
. . . . . . . . . 10
|
23 | 22 | ad2antrl 764 |
. . . . . . . . 9
|
24 | 7, 8, 9, 10, 11, 2 | elqaalem1 24074 |
. . . . . . . . . . 11
|
25 | 24 | simpld 475 |
. . . . . . . . . 10
|
26 | 25 | adantr 481 |
. . . . . . . . 9
|
27 | 23, 26 | zmodcld 12691 |
. . . . . . . 8
|
28 | 27 | nn0zd 11480 |
. . . . . . 7
|
29 | | nnz 11399 |
. . . . . . . . . 10
|
30 | 29 | ad2antll 765 |
. . . . . . . . 9
|
31 | 30, 26 | zmodcld 12691 |
. . . . . . . 8
|
32 | 31 | nn0zd 11480 |
. . . . . . 7
|
33 | 26 | nnrpd 11870 |
. . . . . . 7
|
34 | | nnre 11027 |
. . . . . . . . 9
|
35 | 34 | ad2antrl 764 |
. . . . . . . 8
|
36 | | modabs2 12704 |
. . . . . . . 8
|
37 | 35, 33, 36 | syl2anc 693 |
. . . . . . 7
|
38 | | nnre 11027 |
. . . . . . . . 9
|
39 | 38 | ad2antll 765 |
. . . . . . . 8
|
40 | | modabs2 12704 |
. . . . . . . 8
|
41 | 39, 33, 40 | syl2anc 693 |
. . . . . . 7
|
42 | 28, 23, 32, 30, 33, 37, 41 | modmul12d 12724 |
. . . . . 6
|
43 | | oveq1 6657 |
. . . . . . . . . 10
|
44 | | eqid 2622 |
. . . . . . . . . 10
|
45 | | ovex 6678 |
. . . . . . . . . 10
|
46 | 43, 44, 45 | fvmpt 6282 |
. . . . . . . . 9
|
47 | 46 | ad2antrl 764 |
. . . . . . . 8
|
48 | | oveq1 6657 |
. . . . . . . . . 10
|
49 | | ovex 6678 |
. . . . . . . . . 10
|
50 | 48, 44, 49 | fvmpt 6282 |
. . . . . . . . 9
|
51 | 50 | ad2antll 765 |
. . . . . . . 8
|
52 | 47, 51 | oveq12d 6668 |
. . . . . . 7
|
53 | | oveq12 6659 |
. . . . . . . . . 10
|
54 | 53 | oveq1d 6665 |
. . . . . . . . 9
|
55 | | elqaa.7 |
. . . . . . . . 9
|
56 | | ovex 6678 |
. . . . . . . . 9
|
57 | 54, 55, 56 | ovmpt2a 6791 |
. . . . . . . 8
|
58 | 45, 49, 57 | mp2an 708 |
. . . . . . 7
|
59 | 52, 58 | syl6eq 2672 |
. . . . . 6
|
60 | | oveq1 6657 |
. . . . . . . 8
|
61 | | ovex 6678 |
. . . . . . . 8
|
62 | 60, 44, 61 | fvmpt 6282 |
. . . . . . 7
|
63 | 5, 62 | syl 17 |
. . . . . 6
|
64 | 42, 59, 63 | 3eqtr4rd 2667 |
. . . . 5
|
65 | | oveq1 6657 |
. . . . . . . . 9
|
66 | | ovex 6678 |
. . . . . . . . 9
|
67 | 65, 44, 66 | fvmpt 6282 |
. . . . . . . 8
|
68 | 14, 67 | syl 17 |
. . . . . . 7
|
69 | | fveq2 6191 |
. . . . . . . . . 10
|
70 | 69 | oveq1d 6665 |
. . . . . . . . 9
|
71 | | eqid 2622 |
. . . . . . . . 9
|
72 | 70, 71, 66 | fvmpt 6282 |
. . . . . . . 8
|
73 | 72 | adantl 482 |
. . . . . . 7
|
74 | 68, 73 | eqtr4d 2659 |
. . . . . 6
|
75 | 6, 74 | sylan2 491 |
. . . . 5
deg |
76 | 5, 15, 21, 64, 75 | seqhomo 12848 |
. . . 4
deg deg |
77 | 3, 76 | syl5eq 2668 |
. . 3
deg |
78 | 1, 77 | sylan2 491 |
. 2
deg
deg |
79 | | 0zd 11389 |
. . . . . . . 8
|
80 | 4 | adantl 482 |
. . . . . . . 8
|
81 | 19, 79, 13, 80 | seqf 12822 |
. . . . . . 7
|
82 | 81, 18 | ffvelrnd 6360 |
. . . . . 6
deg |
83 | 2, 82 | syl5eqel 2705 |
. . . . 5
|
84 | 83 | adantr 481 |
. . . 4
|
85 | | oveq1 6657 |
. . . . 5
|
86 | | ovex 6678 |
. . . . 5
|
87 | 85, 44, 86 | fvmpt 6282 |
. . . 4
|
88 | 84, 87 | syl 17 |
. . 3
|
89 | 1, 88 | sylan2 491 |
. 2
deg |
90 | | vex 3203 |
. . . . 5
|
91 | | vex 3203 |
. . . . 5
|
92 | | oveq12 6659 |
. . . . . . 7
|
93 | 92 | oveq1d 6665 |
. . . . . 6
|
94 | 93, 55, 61 | ovmpt2a 6791 |
. . . . 5
|
95 | 90, 91, 94 | mp2an 708 |
. . . 4
|
96 | | nn0mulcl 11329 |
. . . . . 6
|
97 | 96 | nn0zd 11480 |
. . . . 5
|
98 | 1, 25 | sylan2 491 |
. . . . 5
deg |
99 | | zmodcl 12690 |
. . . . 5
|
100 | 97, 98, 99 | syl2anr 495 |
. . . 4
deg
|
101 | 95, 100 | syl5eqel 2705 |
. . 3
deg
|
102 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
105 | 104 | rabbidv 3189 |
. . . . . . . . . . . . . 14
|
106 | 105 | infeq1d 8383 |
. . . . . . . . . . . . 13
inf inf |
107 | 106 | cbvmptv 4750 |
. . . . . . . . . . . 12
inf
inf |
108 | 11, 107 | eqtri 2644 |
. . . . . . . . . . 11
inf
|
109 | 7, 8, 9, 10, 108, 2 | elqaalem1 24074 |
. . . . . . . . . 10
|
110 | 109 | simpld 475 |
. . . . . . . . 9
|
111 | 110 | adantlr 751 |
. . . . . . . 8
|
112 | 111 | nnzd 11481 |
. . . . . . 7
|
113 | 25 | adantr 481 |
. . . . . . 7
|
114 | 112, 113 | zmodcld 12691 |
. . . . . 6
|
115 | 114, 71 | fmptd 6385 |
. . . . 5
|
116 | 1, 115 | sylan2 491 |
. . . 4
deg |
117 | | ffvelrn 6357 |
. . . 4
|
118 | 116, 6, 117 | syl2an 494 |
. . 3
deg deg
|
119 | | c0ex 10034 |
. . . . 5
|
120 | | oveq12 6659 |
. . . . . . 7
|
121 | 120 | oveq1d 6665 |
. . . . . 6
|
122 | | ovex 6678 |
. . . . . 6
|
123 | 121, 55, 122 | ovmpt2a 6791 |
. . . . 5
|
124 | 119, 90, 123 | mp2an 708 |
. . . 4
|
125 | | nn0cn 11302 |
. . . . . . 7
|
126 | 125 | mul02d 10234 |
. . . . . 6
|
127 | 126 | oveq1d 6665 |
. . . . 5
|
128 | 98 | nnrpd 11870 |
. . . . . 6
deg |
129 | | 0mod 12701 |
. . . . . 6
|
130 | 128, 129 | syl 17 |
. . . . 5
deg |
131 | 127, 130 | sylan9eqr 2678 |
. . . 4
deg |
132 | 124, 131 | syl5eq 2668 |
. . 3
deg |
133 | | oveq12 6659 |
. . . . . . 7
|
134 | 133 | oveq1d 6665 |
. . . . . 6
|
135 | | ovex 6678 |
. . . . . 6
|
136 | 134, 55, 135 | ovmpt2a 6791 |
. . . . 5
|
137 | 90, 119, 136 | mp2an 708 |
. . . 4
|
138 | 125 | mul01d 10235 |
. . . . . 6
|
139 | 138 | oveq1d 6665 |
. . . . 5
|
140 | 139, 130 | sylan9eqr 2678 |
. . . 4
deg |
141 | 137, 140 | syl5eq 2668 |
. . 3
deg |
142 | | simpr 477 |
. . 3
deg deg |
143 | 18 | adantr 481 |
. . 3
deg deg |
144 | 1 | adantl 482 |
. . . . 5
deg |
145 | | fveq2 6191 |
. . . . . . 7
|
146 | 145 | oveq1d 6665 |
. . . . . 6
|
147 | | ovex 6678 |
. . . . . 6
|
148 | 146, 71, 147 | fvmpt 6282 |
. . . . 5
|
149 | 144, 148 | syl 17 |
. . . 4
deg
|
150 | 98 | nncnd 11036 |
. . . . . . 7
deg |
151 | 98 | nnne0d 11065 |
. . . . . . 7
deg |
152 | 150, 151 | dividd 10799 |
. . . . . 6
deg |
153 | | 1z 11407 |
. . . . . 6
|
154 | 152, 153 | syl6eqel 2709 |
. . . . 5
deg |
155 | 98 | nnred 11035 |
. . . . . 6
deg |
156 | | mod0 12675 |
. . . . . 6
|
157 | 155, 128,
156 | syl2anc 693 |
. . . . 5
deg |
158 | 154, 157 | mpbird 247 |
. . . 4
deg |
159 | 149, 158 | eqtrd 2656 |
. . 3
deg
|
160 | 101, 118,
132, 141, 142, 143, 159 | seqz 12849 |
. 2
deg deg |
161 | 78, 89, 160 | 3eqtr3d 2664 |
1
deg |