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 26205

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**
Step	Hyp	Ref	Expression
1		eldiophelnn0 26196	. . 3 Dioph
2		id1 22	. . . . . 6
3		zex 9986	. . . . . . 7
4		difexg 4122	. . . . . . 7 $\$
5	3, 4	mp1i 13	. . . . . 6 $\$
6		ominf 7029	. . . . . . 7
7		nn0z 9999	. . . . . . . 8
8		lzenom 26202	. . . . . . . 8 $\$
9		enfi 7033	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 20	. . . . . . 7 $\$
11	6, 10	mtbiri 296	. . . . . 6 $\$
12		fz1eqin 26201	. . . . . . 7 $\$
13		inss1 3350	. . . . . . . 8 $\$ $\$
14	13	a1i 12	. . . . . . 7 $\$ $\$
15	12, 14	eqsstrd 3173	. . . . . 6 $\$
16		eldioph2b 26195	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
17	2, 5, 11, 15, 16	syl22anc 1188	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
18		nnex 9706	. . . . . . 7
19	18	a1i 12	. . . . . 6
20		1z 10006	. . . . . . 7
21		nnuz 10216	. . . . . . . 8
22	21	uzinf 10980	. . . . . . 7
23	20, 22	mp1i 13	. . . . . 6
24		elfznn 10771	. . . . . . . 8
25	24	ssriv 3145	. . . . . . 7
26	25	a1i 12	. . . . . 6
27		eldioph2b 26195	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
28	2, 19, 23, 26, 27	syl22anc 1188	. . . . 5 Dioph mzPoly $/\$
29	17, 28	anbi12d 694	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		reeanv 2680	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
31		inab 3397	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		reeanv 2680	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33		simplrl 739	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34		simplrr 740	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	12	eqcomd 2261	. . . . . . . . . . . . . . . . . . . . 21 $\$
36	35	reseq2d 4929	. . . . . . . . . . . . . . . . . . . 20 $\$
37	36	ad3antrrr 713	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38	35	reseq2d 4929	. . . . . . . . . . . . . . . . . . . . 21 $\$
39	38	ad3antrrr 713	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
40		simprrl 743	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		simprll 741	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	39, 40, 41	3eqtr2d 2294	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
43	37, 42	eqtr4d 2291	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
44		elmapresaun 26203	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
45	33, 34, 43, 44	syl3anc 1187	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	21	uneq2i 3287	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
47	20	a1i 12	. . . . . . . . . . . . . . . . . . . . 21
48		nn0p1nn 9956	. . . . . . . . . . . . . . . . . . . . . 22
49	48	nnge1d 9742	. . . . . . . . . . . . . . . . . . . . 21
50		lzunuz 26200	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
51	7, 47, 49, 50	syl3anc 1187	. . . . . . . . . . . . . . . . . . . 20 $\$
52	46, 51	syl5eq 2300	. . . . . . . . . . . . . . . . . . 19 $\$
53	52	oveq2d 5794	. . . . . . . . . . . . . . . . . 18 $\$
54	53	ad3antrrr 713	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	45, 54	eleqtrd 2332	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		unidm 3279	. . . . . . . . . . . . . . . . . . 19
57	41, 40	uneq12d 3291	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	56, 57	syl5eqr 2302	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		resundir 4944	. . . . . . . . . . . . . . . . . 18
60	58, 59	syl6eqr 2306	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		uncom 3280	. . . . . . . . . . . . . . . . . . . . 21
62	61	reseq1i 4925	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
63		incom 3322	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
64	63, 35	syl5eq 2300	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
65	64	reseq2d 4929	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
66	65	ad3antrrr 713	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
67	64	reseq2d 4929	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
68	67	ad3antrrr 713	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	68, 41, 40	3eqtr2d 2294	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
70	66, 69	eqtr4d 2291	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71		elmapresaunres2 26204	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
72	34, 33, 70, 71	syl3anc 1187	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	62, 72	syl5eq 2300	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74	73	fveq2d 5448	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
75		simprlr 742	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	74, 75	eqtrd 2288	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
77		elmapresaunres2 26204	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
78	33, 34, 43, 77	syl3anc 1187	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	fveq2d 5448	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		simprrr 744	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	79, 80	eqtrd 2288	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	60, 76, 81	jca32 523	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
83		reseq1 4923	. . . . . . . . . . . . . . . . . . 19
84	83	eqeq2d 2267	. . . . . . . . . . . . . . . . . 18
85		reseq1 4923	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
86	85	fveq2d 5448	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
87	86	eqeq1d 2264	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
88		reseq1 4923	. . . . . . . . . . . . . . . . . . . . 21
89	88	fveq2d 5448	. . . . . . . . . . . . . . . . . . . 20
90	89	eqeq1d 2264	. . . . . . . . . . . . . . . . . . 19
91	87, 90	anbi12d 694	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
92	84, 91	anbi12d 694	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	92	rcla4ev 2852	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
94	55, 82, 93	syl2anc 645	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	ex 425	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96	95	rexlimdvva 2647	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
97		simpr 449	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
98		difss 3264	. . . . . . . . . . . . . . . . . 18 $\$
99		elmapssres 26145	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
100	97, 98, 99	sylancl 646	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
101	100	adantr 453	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
102		nnssz 9996	. . . . . . . . . . . . . . . . . 18
103		elmapssres 26145	. . . . . . . . . . . . . . . . . 18 $/\$
104	97, 102, 103	sylancl 646	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
105	104	adantr 453	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106		simprl 735	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
107	15	ad3antrrr 713	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
108		resabs1 4958	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110	106, 109	eqtr4d 2291	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111		simprrl 743	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
112	110, 111	jca 520	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
113		resabs1 4958	. . . . . . . . . . . . . . . . . . 19
114	25, 113	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115	106, 114	eqtr4d 2291	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116		simprrr 744	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
117	112, 115, 116	jca32 523	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
118		reseq1 4923	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
119	118	eqeq2d 2267	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
120		fveq2 5444	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
121	120	eqeq1d 2264	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
122	119, 121	anbi12d 694	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
123	122	anbi1d 688	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
124		reseq1 4923	. . . . . . . . . . . . . . . . . . . 20
125	124	eqeq2d 2267	. . . . . . . . . . . . . . . . . . 19
126		fveq2 5444	. . . . . . . . . . . . . . . . . . . 20
127	126	eqeq1d 2264	. . . . . . . . . . . . . . . . . . 19
128	125, 127	anbi12d 694	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	128	anbi2d 687	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
130	123, 129	rcla42ev 2860	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
131	101, 105, 117, 130	syl3anc 1187	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	ex 425	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	132	rexlimdva 2640	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
134	96, 133	impbid 185	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
135		simplrl 739	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
136		mzpf 26167	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
138		nn0ssz 9997	. . . . . . . . . . . . . . . . . . . . . 22
139		mapss 6764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
140	3, 138, 139	mp2an 656	. . . . . . . . . . . . . . . . . . . . 21
141	140	sseli 3137	. . . . . . . . . . . . . . . . . . . 20
142		elmapssres 26145	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
143	141, 98, 142	sylancl 646	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
144	143	adantl 454	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
145		ffvelrn 5583	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$
146	137, 144, 145	syl2anc 645	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
147	146	zred 10070	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
148		simplrr 740	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
149		mzpf 26167	. . . . . . . . . . . . . . . . . . 19 mzPoly
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
151		elmapssres 26145	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	141, 102, 151	sylancl 646	. . . . . . . . . . . . . . . . . . 19
153	152	adantl 454	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		ffvelrn 5583	. . . . . . . . . . . . . . . . . 18 $/\$
155	150, 153, 154	syl2anc 645	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
156	155	zred 10070	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		sumsqeq0 11134	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
158	147, 156, 157	syl2anc 645	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
159	141	adantl 454	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
160		reseq1 4923	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
161	160	fveq2d 5448	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
162	161	oveq1d 5793	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
163		reseq1 4923	. . . . . . . . . . . . . . . . . . . . 21
164	163	fveq2d 5448	. . . . . . . . . . . . . . . . . . . 20
165	164	oveq1d 5793	. . . . . . . . . . . . . . . . . . 19
166	162, 165	oveq12d 5796	. . . . . . . . . . . . . . . . . 18 $\$ $\$
167		eqid 2256	. . . . . . . . . . . . . . . . . 18 $\$ $\$
168		ovex 5803	. . . . . . . . . . . . . . . . . 18 $\$
169	166, 167, 168	fvmpt 5522	. . . . . . . . . . . . . . . . 17 $\$ $\$
170	159, 169	syl 17	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
171	170	eqeq1d 2264	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
172	158, 171	bitr4d 249	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
173	172	anbi2d 687	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
174	173	rexbidva 2533	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
175	134, 174	bitrd 246	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
176	32, 175	syl5bbr 252	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
177	176	abbidv 2370	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
178	31, 177	syl5eq 2300	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
179		simpl 445	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
180		fzssuz 10784	. . . . . . . . . . . 12
181		uzssz 10200	. . . . . . . . . . . 12
182	180, 181	sstri 3149	. . . . . . . . . . 11
183	3, 182	pm3.2i 443	. . . . . . . . . 10 $/\$
184	183	a1i 12	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
185	3	a1i 12	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
186	98	a1i 12	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
187		simprl 735	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
188		mzpresrename 26181	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
189	185, 186, 187, 188	syl3anc 1187	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
190		2nn0 9935	. . . . . . . . . . 11
191		mzpexpmpt 26176	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
192	189, 190, 191	sylancl 646	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
193	102	a1i 12	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
194		simprr 736	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
195		mzpresrename 26181	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
196	185, 193, 194, 195	syl3anc 1187	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
197		mzpexpmpt 26176	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
198	196, 190, 197	sylancl 646	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
199		mzpaddmpt 26172	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
200	192, 198, 199	syl2anc 645	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
201		eldioph2 26194	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
202	179, 184, 200, 201	syl3anc 1187	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
203	178, 202	eqeltrd 2330	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
204		ineq12 3326	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
205	204	eleq1d 2322	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
206	203, 205	syl5ibrcom 215	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
207	206	rexlimdvva 2647	. . . . 5 mzPoly $\$ mzPoly