Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 37327 |
. . 3
Dioph
|
2 | | id 22 |
. . . . . 6
|
3 | | zex 11386 |
. . . . . . 7
|
4 | | difexg 4808 |
. . . . . . 7
|
5 | 3, 4 | mp1i 13 |
. . . . . 6
|
6 | | ominf 8172 |
. . . . . . 7
|
7 | | nn0z 11400 |
. . . . . . . 8
|
8 | | lzenom 37333 |
. . . . . . . 8
|
9 | | enfi 8176 |
. . . . . . . 8
|
10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
|
11 | 6, 10 | mtbiri 317 |
. . . . . 6
|
12 | | fz1eqin 37332 |
. . . . . . 7
|
13 | | inss1 3833 |
. . . . . . 7
|
14 | 12, 13 | syl6eqss 3655 |
. . . . . 6
|
15 | | eldioph2b 37326 |
. . . . . 6
Dioph
mzPoly
|
16 | 2, 5, 11, 14, 15 | syl22anc 1327 |
. . . . 5
Dioph mzPoly
|
17 | | nnex 11026 |
. . . . . . 7
|
18 | 17 | a1i 11 |
. . . . . 6
|
19 | | 1z 11407 |
. . . . . . 7
|
20 | | nnuz 11723 |
. . . . . . . 8
|
21 | 20 | uzinf 12764 |
. . . . . . 7
|
22 | 19, 21 | mp1i 13 |
. . . . . 6
|
23 | | elfznn 12370 |
. . . . . . . 8
|
24 | 23 | ssriv 3607 |
. . . . . . 7
|
25 | 24 | a1i 11 |
. . . . . 6
|
26 | | eldioph2b 37326 |
. . . . . 6
Dioph mzPoly
|
27 | 2, 18, 22, 25, 26 | syl22anc 1327 |
. . . . 5
Dioph mzPoly
|
28 | 16, 27 | anbi12d 747 |
. . . 4
Dioph Dioph mzPoly
mzPoly
|
29 | | reeanv 3107 |
. . . . 5
mzPoly
mzPoly
mzPoly
mzPoly
|
30 | | inab 3895 |
. . . . . . . . 9
|
31 | | reeanv 3107 |
. . . . . . . . . . 11
|
32 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
33 | | simplrr 801 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
34 | 12 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | 34 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
37 | 34 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 37 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
39 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
40 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
41 | 38, 39, 40 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
42 | 36, 41 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
43 | | elmapresaun 37334 |
. . . . . . . . . . . . . . . . . 18
|
44 | 32, 33, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
45 | 20 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | 47 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | | lzunuz 37331 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | 7, 46, 48, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 45, 50 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
54 | 44, 53 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
|
55 | | unidm 3756 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 40, 39 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
57 | 55, 56 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
58 | | resundir 5411 |
. . . . . . . . . . . . . . . . . 18
|
59 | 57, 58 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
60 | | uncom 3757 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 60 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
63 | 62, 34 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | 63 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 64 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly mzPoly
|
66 | 63 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
67 | 66 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
mzPoly mzPoly
|
68 | 67, 40, 39 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . . . . 22
mzPoly mzPoly
|
69 | 65, 68 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . 21
mzPoly mzPoly
|
70 | | elmapresaunres2 37335 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 33, 32, 69, 70 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
72 | 61, 71 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
74 | | simprlr 803 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
75 | 73, 74 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
76 | | elmapresaunres2 37335 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 32, 33, 42, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
79 | | simprrr 805 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
80 | 78, 79 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
81 | 59, 75, 80 | jca32 558 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
|
82 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
84 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 84 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 85 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
|
87 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 86, 89 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
91 | 83, 90 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
92 | 91 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
|
93 | 54, 81, 92 | syl2anc 693 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly
|
94 | 93 | ex 450 |
. . . . . . . . . . . . . 14
mzPoly mzPoly
|
95 | 94 | rexlimdvva 3038 |
. . . . . . . . . . . . 13
mzPoly mzPoly
|
96 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly |
97 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
|
98 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . 18
|
99 | 96, 97, 98 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
|
101 | | nnssz 11397 |
. . . . . . . . . . . . . . . . . 18
|
102 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . 18
|
103 | 96, 101, 102 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly |
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly |
105 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly |
106 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
mzPoly mzPoly
|
107 | 106 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly
|
108 | 105, 107 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
109 | | simprrl 804 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly |
110 | 108, 109 | jca 554 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
111 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 24, 111 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
113 | 105, 112 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly
|
114 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly |
115 | 110, 113,
114 | jca32 558 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
|
116 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . 20
|
117 | 116 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
118 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 118 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 117, 119 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
121 | 120 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
|
122 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . 20
|
123 | 122 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
124 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
125 | 124 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
|
126 | 123, 125 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
127 | 126 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
|
128 | 121, 127 | rspc2ev 3324 |
. . . . . . . . . . . . . . . 16
|
129 | 100, 104,
115, 128 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly
|
130 | 129 | ex 450 |
. . . . . . . . . . . . . 14
mzPoly mzPoly
|
131 | 130 | rexlimdva 3031 |
. . . . . . . . . . . . 13
mzPoly mzPoly
|
132 | 95, 131 | impbid 202 |
. . . . . . . . . . . 12
mzPoly mzPoly
|
133 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly mzPoly |
134 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . 19
mzPoly
|
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
136 | | nn0ssz 11398 |
. . . . . . . . . . . . . . . . . . . . . 22
|
137 | | mapss 7900 |
. . . . . . . . . . . . . . . . . . . . . 22
|
138 | 3, 136, 137 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
|
139 | 138 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 139, 97, 140 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly
|
143 | 135, 142 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly |
144 | 143 | zred 11482 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly |
145 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
mzPoly mzPoly mzPoly |
146 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . 19
mzPoly |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly |
148 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | 139, 101,
148 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
mzPoly mzPoly |
151 | 147, 150 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly |
152 | 151 | zred 11482 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly |
153 | | sumsqeq0 12942 |
. . . . . . . . . . . . . . . 16
|
154 | 144, 152,
153 | syl2anc 693 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly
|
155 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . 17
mzPoly mzPoly |
156 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
158 | 157 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
159 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
|
160 | 159 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 160 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 158, 161 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
163 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
164 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
|
165 | 162, 163,
164 | fvmpt 6282 |
. . . . . . . . . . . . . . . . 17
|
166 | 155, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
mzPoly mzPoly
|
167 | 166 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
mzPoly mzPoly |
168 | 154, 167 | bitr4d 271 |
. . . . . . . . . . . . . 14
mzPoly mzPoly
|
169 | 168 | anbi2d 740 |
. . . . . . . . . . . . 13
mzPoly mzPoly
|
170 | 169 | rexbidva 3049 |
. . . . . . . . . . . 12
mzPoly mzPoly
|
171 | 132, 170 | bitrd 268 |
. . . . . . . . . . 11
mzPoly mzPoly
|
172 | 31, 171 | syl5bbr 274 |
. . . . . . . . . 10
mzPoly mzPoly
|
173 | 172 | abbidv 2741 |
. . . . . . . . 9
mzPoly mzPoly
|
174 | 30, 173 | syl5eq 2668 |
. . . . . . . 8
mzPoly mzPoly
|
175 | | simpl 473 |
. . . . . . . . 9
mzPoly mzPoly |
176 | | fzssuz 12382 |
. . . . . . . . . . . 12
|
177 | | uzssz 11707 |
. . . . . . . . . . . 12
|
178 | 176, 177 | sstri 3612 |
. . . . . . . . . . 11
|
179 | 3, 178 | pm3.2i 471 |
. . . . . . . . . 10
|
180 | 179 | a1i 11 |
. . . . . . . . 9
mzPoly mzPoly |
181 | 3 | a1i 11 |
. . . . . . . . . . . 12
mzPoly mzPoly |
182 | 97 | a1i 11 |
. . . . . . . . . . . 12
mzPoly mzPoly
|
183 | | simprl 794 |
. . . . . . . . . . . 12
mzPoly mzPoly mzPoly |
184 | | mzpresrename 37313 |
. . . . . . . . . . . 12
mzPoly mzPoly |
185 | 181, 182,
183, 184 | syl3anc 1326 |
. . . . . . . . . . 11
mzPoly mzPoly mzPoly |
186 | | 2nn0 11309 |
. . . . . . . . . . 11
|
187 | | mzpexpmpt 37308 |
. . . . . . . . . . 11
mzPoly
mzPoly |
188 | 185, 186,
187 | sylancl 694 |
. . . . . . . . . 10
mzPoly mzPoly mzPoly |
189 | 101 | a1i 11 |
. . . . . . . . . . . 12
mzPoly mzPoly |
190 | | simprr 796 |
. . . . . . . . . . . 12
mzPoly mzPoly mzPoly |
191 | | mzpresrename 37313 |
. . . . . . . . . . . 12
mzPoly
mzPoly |
192 | 181, 189,
190, 191 | syl3anc 1326 |
. . . . . . . . . . 11
mzPoly mzPoly mzPoly |
193 | | mzpexpmpt 37308 |
. . . . . . . . . . 11
mzPoly
mzPoly |
194 | 192, 186,
193 | sylancl 694 |
. . . . . . . . . 10
mzPoly mzPoly mzPoly |
195 | | mzpaddmpt 37304 |
. . . . . . . . . 10
mzPoly mzPoly
mzPoly |
196 | 188, 194,
195 | syl2anc 693 |
. . . . . . . . 9
mzPoly mzPoly
mzPoly |
197 | | eldioph2 37325 |
. . . . . . . . 9
mzPoly
Dioph |
198 | 175, 180,
196, 197 | syl3anc 1326 |
. . . . . . . 8
mzPoly mzPoly
Dioph |
199 | 174, 198 | eqeltrd 2701 |
. . . . . . 7
mzPoly mzPoly
Dioph |
200 | | ineq12 3809 |
. . . . . . . 8
|
201 | 200 | eleq1d 2686 |
. . . . . . 7
Dioph
Dioph |
202 | 199, 201 | syl5ibrcom 237 |
. . . . . 6
mzPoly mzPoly
Dioph |
203 | 202 | rexlimdvva 3038 |
. . . . 5
mzPoly
mzPoly
Dioph |
204 | 29, 203 | syl5bir 233 |
. . . 4
mzPoly
mzPoly
Dioph |
205 | 28, 204 | sylbid 230 |
. . 3
Dioph Dioph
Dioph |
206 | 1, 205 | syl 17 |
. 2
Dioph
Dioph
Dioph Dioph |
207 | 206 | anabsi5 858 |
1
Dioph Dioph
Dioph |