diophin - Mathbox for Stefan O'Rear

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

Theorem diophin 35686

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 35677	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10970	. . . . . . 7
4		difexg 4545	. . . . . . 7 $\$
5	3, 4	mp1i 13	. . . . . 6 $\$
6		ominf 7802	. . . . . . 7
7		nn0z 10984	. . . . . . . 8
8		lzenom 35683	. . . . . . . 8 $\$
9		enfi 7806	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 18	. . . . . . 7 $\$
11	6, 10	mtbiri 310	. . . . . 6 $\$
12		fz1eqin 35682	. . . . . . 7 $\$
13		inss1 3643	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3468	. . . . . 6 $\$
15		eldioph2b 35676	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1293	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10637	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10991	. . . . . . 7
20		nnuz 11218	. . . . . . . 8
21	20	uzinf 12217	. . . . . . 7
22	19, 21	mp1i 13	. . . . . 6
23		elfznn 11854	. . . . . . . 8
24	23	ssriv 3422	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 35676	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1293	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 725	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 2944	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3702	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 2944	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 778	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 779	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5111	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 744	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5111	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 782	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 780	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2511	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2508	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 35684	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1292	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3576	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10933	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10674	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 35681	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1292	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2517	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 744	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2551	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3568	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3580	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2519	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5125	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2523	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3569	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5107	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3616	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2517	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5111	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5111	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2511	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2508	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 35685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1292	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2517	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 781	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 35685	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1292	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 783	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 544	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5105	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18
84		reseq1 5105	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2473	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5105	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2473	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 725	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 725	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3136	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 441	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2878	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 468	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3549	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7514	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 675	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10981	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7514	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 675	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 772	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107	106	resabs1d 5140	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
108	105, 107	eqtr4d 2508	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109		simprrl 782	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110	108, 109	jca 541	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
111		resabs1 5139	. . . . . . . . . . . . . . . . . . 19
112	24, 111	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
113	105, 112	eqtr4d 2508	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114		simprrr 783	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115	110, 113, 114	jca32 544	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
116		reseq1 5105	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
117	116	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
118		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
119	118	eqeq1d 2473	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
120	117, 119	anbi12d 725	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
121	120	anbi1d 719	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
122		reseq1 5105	. . . . . . . . . . . . . . . . . . . 20
123	122	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
124		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
125	124	eqeq1d 2473	. . . . . . . . . . . . . . . . . . 19
126	123, 125	anbi12d 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	126	anbi2d 718	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
128	121, 127	rspc2ev 3149	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
129	100, 104, 115, 128	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
130	129	ex 441	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	rexlimdva 2871	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	95, 131	impbid 195	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
133		simplrl 778	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
134		mzpf 35649	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
136		nn0ssz 10982	. . . . . . . . . . . . . . . . . . . . . 22
137		mapss 7532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	3, 136, 137	mp2an 686	. . . . . . . . . . . . . . . . . . . . 21
139	138	sseli 3414	. . . . . . . . . . . . . . . . . . . 20
140		elmapssres 7514	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
141	139, 97, 140	sylancl 675	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
142	141	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
143	135, 142	ffvelrnd 6038	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
144	143	zred 11063	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145		simplrr 779	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
146		mzpf 35649	. . . . . . . . . . . . . . . . . . 19 mzPoly
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
148		elmapssres 7514	. . . . . . . . . . . . . . . . . . . 20 $/\$
149	139, 101, 148	sylancl 675	. . . . . . . . . . . . . . . . . . 19
150	149	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
151	147, 150	ffvelrnd 6038	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	151	zred 11063	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153		sumsqeq0 12391	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
154	144, 152, 153	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
155	139	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
156		reseq1 5105	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
157	156	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
158	157	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
159		reseq1 5105	. . . . . . . . . . . . . . . . . . . . 21
160	159	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
161	160	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
162	158, 161	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 $\$ $\$
163		eqid 2471	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		ovex 6336	. . . . . . . . . . . . . . . . . 18 $\$
165	162, 163, 164	fvmpt 5963	. . . . . . . . . . . . . . . . 17 $\$ $\$
166	155, 165	syl 17	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
167	166	eqeq1d 2473	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	154, 167	bitr4d 264	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
169	168	anbi2d 718	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
170	169	rexbidva 2889	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
171	132, 170	bitrd 261	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
172	31, 171	syl5bbr 267	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	172	abbidv 2589	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	30, 173	syl5eq 2517	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
175		simpl 464	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
176		fzssuz 11865	. . . . . . . . . . . 12
177		uzssz 11202	. . . . . . . . . . . 12
178	176, 177	sstri 3427	. . . . . . . . . . 11
179	3, 178	pm3.2i 462	. . . . . . . . . 10 $/\$
180	179	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
181	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
182	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
183		simprl 772	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
184		mzpresrename 35663	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
185	181, 182, 183, 184	syl3anc 1292	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
186		2nn0 10910	. . . . . . . . . . 11
187		mzpexpmpt 35658	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
188	185, 186, 187	sylancl 675	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
189	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
190		simprr 774	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
191		mzpresrename 35663	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
192	181, 189, 190, 191	syl3anc 1292	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
193		mzpexpmpt 35658	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
194	192, 186, 193	sylancl 675	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
195		mzpaddmpt 35654	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
196	188, 194, 195	syl2anc 673	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
197		eldioph2 35675	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
198	175, 180, 196, 197	syl3anc 1292	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
199	174, 198	eqeltrd 2549	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
200		ineq12 3620	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
201	200	eleq1d 2533	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
202	199, 201	syl5ibrcom 230	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
203	202	rexlimdvva 2878	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	29, 203	syl5bir 226	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$ Dioph
205	28, 204	sylbid 223	. . 3