diophin - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > diophin		Unicode version

Theorem diophin 26852

Description: If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)

**Assertion**
Ref	Expression
diophin	Dioph $/\$ Dioph Dioph

Proof of Theorem diophin Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldiophelnn0 26843	. . 3 Dioph
2		id 19	. . . . . 6
3		zex 10033	. . . . . . 7
4		difexg 4162	. . . . . . 7 $\$
5	3, 4	mp1i 11	. . . . . 6 $\$
6		ominf 7075	. . . . . . 7
7		nn0z 10046	. . . . . . . 8
8		lzenom 26849	. . . . . . . 8 $\$
9		enfi 7079	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 18	. . . . . . 7 $\$
11	6, 10	mtbiri 294	. . . . . 6 $\$
12		fz1eqin 26848	. . . . . . 7 $\$
13		inss1 3389	. . . . . . . 8 $\$ $\$
14	13	a1i 10	. . . . . . 7 $\$ $\$
15	12, 14	eqsstrd 3212	. . . . . 6 $\$
16		eldioph2b 26842	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
17	2, 5, 11, 15, 16	syl22anc 1183	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
18		nnex 9752	. . . . . . 7
19	18	a1i 10	. . . . . 6
20		1z 10053	. . . . . . 7
21		nnuz 10263	. . . . . . . 8
22	21	uzinf 11028	. . . . . . 7
23	20, 22	mp1i 11	. . . . . 6
24		elfznn 10819	. . . . . . . 8
25	24	ssriv 3184	. . . . . . 7
26	25	a1i 10	. . . . . 6
27		eldioph2b 26842	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
28	2, 19, 23, 26, 27	syl22anc 1183	. . . . 5 Dioph mzPoly $/\$
29	17, 28	anbi12d 691	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		reeanv 2707	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
31		inab 3436	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		reeanv 2707	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33		simplrl 736	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34		simplrr 737	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	12	eqcomd 2288	. . . . . . . . . . . . . . . . . . . . 21 $\$
36	35	reseq2d 4955	. . . . . . . . . . . . . . . . . . . 20 $\$
37	36	ad3antrrr 710	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38	35	reseq2d 4955	. . . . . . . . . . . . . . . . . . . . 21 $\$
39	38	ad3antrrr 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
40		simprrl 740	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		simprll 738	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	39, 40, 41	3eqtr2d 2321	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
43	37, 42	eqtr4d 2318	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
44		elmapresaun 26850	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
45	33, 34, 43, 44	syl3anc 1182	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	21	uneq2i 3326	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
47	20	a1i 10	. . . . . . . . . . . . . . . . . . . . 21
48		nn0p1nn 10003	. . . . . . . . . . . . . . . . . . . . . 22
49	48	nnge1d 9788	. . . . . . . . . . . . . . . . . . . . 21
50		lzunuz 26847	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
51	7, 47, 49, 50	syl3anc 1182	. . . . . . . . . . . . . . . . . . . 20 $\$
52	46, 51	syl5eq 2327	. . . . . . . . . . . . . . . . . . 19 $\$
53	52	oveq2d 5874	. . . . . . . . . . . . . . . . . 18 $\$
54	53	ad3antrrr 710	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	45, 54	eleqtrd 2359	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		unidm 3318	. . . . . . . . . . . . . . . . . . 19
57	41, 40	uneq12d 3330	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	56, 57	syl5eqr 2329	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		resundir 4970	. . . . . . . . . . . . . . . . . 18
60	58, 59	syl6eqr 2333	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		uncom 3319	. . . . . . . . . . . . . . . . . . . . 21
62	61	reseq1i 4951	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
63		incom 3361	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
64	63, 35	syl5eq 2327	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
65	64	reseq2d 4955	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
66	65	ad3antrrr 710	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
67	64	reseq2d 4955	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
68	67	ad3antrrr 710	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	68, 41, 40	3eqtr2d 2321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
70	66, 69	eqtr4d 2318	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71		elmapresaunres2 26851	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
72	34, 33, 70, 71	syl3anc 1182	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	62, 72	syl5eq 2327	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74	73	fveq2d 5529	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
75		simprlr 739	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	74, 75	eqtrd 2315	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
77		elmapresaunres2 26851	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
78	33, 34, 43, 77	syl3anc 1182	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	fveq2d 5529	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		simprrr 741	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	79, 80	eqtrd 2315	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	60, 76, 81	jca32 521	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
83		reseq1 4949	. . . . . . . . . . . . . . . . . . 19
84	83	eqeq2d 2294	. . . . . . . . . . . . . . . . . 18
85		reseq1 4949	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
86	85	fveq2d 5529	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
87	86	eqeq1d 2291	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
88		reseq1 4949	. . . . . . . . . . . . . . . . . . . . 21
89	88	fveq2d 5529	. . . . . . . . . . . . . . . . . . . 20
90	89	eqeq1d 2291	. . . . . . . . . . . . . . . . . . 19
91	87, 90	anbi12d 691	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
92	84, 91	anbi12d 691	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	92	rspcev 2884	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
94	55, 82, 93	syl2anc 642	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	ex 423	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96	95	rexlimdvva 2674	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
97		simpr 447	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
98		difss 3303	. . . . . . . . . . . . . . . . . 18 $\$
99		elmapssres 26792	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
100	97, 98, 99	sylancl 643	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
101	100	adantr 451	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
102		nnssz 10043	. . . . . . . . . . . . . . . . . 18
103		elmapssres 26792	. . . . . . . . . . . . . . . . . 18 $/\$
104	97, 102, 103	sylancl 643	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
105	104	adantr 451	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106		simprl 732	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
107	15	ad3antrrr 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
108		resabs1 4984	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
109	107, 108	syl 15	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110	106, 109	eqtr4d 2318	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111		simprrl 740	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
112	110, 111	jca 518	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
113		resabs1 4984	. . . . . . . . . . . . . . . . . . 19
114	25, 113	mp1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115	106, 114	eqtr4d 2318	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116		simprrr 741	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
117	112, 115, 116	jca32 521	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
118		reseq1 4949	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
119	118	eqeq2d 2294	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
120		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
121	120	eqeq1d 2291	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
122	119, 121	anbi12d 691	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
123	122	anbi1d 685	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
124		reseq1 4949	. . . . . . . . . . . . . . . . . . . 20
125	124	eqeq2d 2294	. . . . . . . . . . . . . . . . . . 19
126		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20
127	126	eqeq1d 2291	. . . . . . . . . . . . . . . . . . 19
128	125, 127	anbi12d 691	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	128	anbi2d 684	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
130	123, 129	rspc2ev 2892	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
131	101, 105, 117, 130	syl3anc 1182	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	ex 423	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	132	rexlimdva 2667	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
134	96, 133	impbid 183	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
135		simplrl 736	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
136		mzpf 26814	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
137	135, 136	syl 15	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
138		nn0ssz 10044	. . . . . . . . . . . . . . . . . . . . . 22
139		mapss 6810	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
140	3, 138, 139	mp2an 653	. . . . . . . . . . . . . . . . . . . . 21
141	140	sseli 3176	. . . . . . . . . . . . . . . . . . . 20
142		elmapssres 26792	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
143	141, 98, 142	sylancl 643	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
144	143	adantl 452	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
145		ffvelrn 5663	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$
146	137, 144, 145	syl2anc 642	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
147	146	zred 10117	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
148		simplrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
149		mzpf 26814	. . . . . . . . . . . . . . . . . . 19 mzPoly
150	148, 149	syl 15	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
151		elmapssres 26792	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	141, 102, 151	sylancl 643	. . . . . . . . . . . . . . . . . . 19
153	152	adantl 452	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		ffvelrn 5663	. . . . . . . . . . . . . . . . . 18 $/\$
155	150, 153, 154	syl2anc 642	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
156	155	zred 10117	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		sumsqeq0 11182	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
158	147, 156, 157	syl2anc 642	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
159	141	adantl 452	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
160		reseq1 4949	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
161	160	fveq2d 5529	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
162	161	oveq1d 5873	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
163		reseq1 4949	. . . . . . . . . . . . . . . . . . . . 21
164	163	fveq2d 5529	. . . . . . . . . . . . . . . . . . . 20
165	164	oveq1d 5873	. . . . . . . . . . . . . . . . . . 19
166	162, 165	oveq12d 5876	. . . . . . . . . . . . . . . . . 18 $\$ $\$
167		eqid 2283	. . . . . . . . . . . . . . . . . 18 $\$ $\$
168		ovex 5883	. . . . . . . . . . . . . . . . . 18 $\$
169	166, 167, 168	fvmpt 5602	. . . . . . . . . . . . . . . . 17 $\$ $\$
170	159, 169	syl 15	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
171	170	eqeq1d 2291	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
172	158, 171	bitr4d 247	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
173	172	anbi2d 684	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
174	173	rexbidva 2560	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
175	134, 174	bitrd 244	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
176	32, 175	syl5bbr 250	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
177	176	abbidv 2397	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
178	31, 177	syl5eq 2327	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
179		simpl 443	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
180		fzssuz 10832	. . . . . . . . . . . 12
181		uzssz 10247	. . . . . . . . . . . 12
182	180, 181	sstri 3188	. . . . . . . . . . 11
183	3, 182	pm3.2i 441	. . . . . . . . . 10 $/\$
184	183	a1i 10	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
185	3	a1i 10	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
186	98	a1i 10	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
187		simprl 732	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
188		mzpresrename 26828	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
189	185, 186, 187, 188	syl3anc 1182	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
190		2nn0 9982	. . . . . . . . . . 11
191		mzpexpmpt 26823	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
192	189, 190, 191	sylancl 643	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
193	102	a1i 10	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
194		simprr 733	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
195		mzpresrename 26828	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
196	185, 193, 194, 195	syl3anc 1182	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
197		mzpexpmpt 26823	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
198	196, 190, 197	sylancl 643	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
199		mzpaddmpt 26819	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
200	192, 198, 199	syl2anc 642	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
201		eldioph2 26841	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
202	179, 184, 200, 201	syl3anc 1182	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
203	178, 202	eqeltrd 2357	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
204		ineq12 3365	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
205	204	eleq1d 2349	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
206	203, 205	syl5ibrcom 213	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
207	206	rexlimdvva 2674	. . . . 5