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 Unicode version

Theorem diophin 29116

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 29107	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10660	. . . . . . 7
4		difexg 4445	. . . . . . 7 $\$
5	3, 4	mp1i 12	. . . . . 6 $\$
6		ominf 7530	. . . . . . 7
7		nn0z 10674	. . . . . . . 8
8		lzenom 29113	. . . . . . . 8 $\$
9		enfi 7534	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 20	. . . . . . 7 $\$
11	6, 10	mtbiri 303	. . . . . 6 $\$
12		fz1eqin 29112	. . . . . . 7 $\$
13		inss1 3575	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3411	. . . . . 6 $\$
15		eldioph2b 29106	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1219	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10333	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10681	. . . . . . 7
20		nnuz 10901	. . . . . . . 8
21	20	uzinf 11793	. . . . . . 7
22	19, 21	mp1i 12	. . . . . 6
23		elfznn 11483	. . . . . . . 8
24	23	ssriv 3365	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 29106	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1219	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 710	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 2893	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3623	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 2893	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 760	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2448	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5115	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5115	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 761	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2481	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2478	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 29114	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1218	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3512	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10624	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10369	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 29111	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1218	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2487	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2519	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3504	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3516	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2489	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5130	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2493	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3505	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5111	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3548	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2487	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5115	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2478	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 29115	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1218	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2487	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5700	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 762	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2475	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 29115	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5700	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 764	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2475	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 535	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5109	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2454	. . . . . . . . . . . . . . . . . 18
84		reseq1 5109	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5700	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5109	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5700	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3078	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2853	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3488	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7242	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10671	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7242	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 755	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		resabs1 5144	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
108	106, 107	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	105, 108	eqtr4d 2478	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110		simprrl 763	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111	109, 110	jca 532	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
112		resabs1 5144	. . . . . . . . . . . . . . . . . . 19
113	24, 112	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114	105, 113	eqtr4d 2478	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115		simprrr 764	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116	111, 114, 115	jca32 535	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
117		reseq1 5109	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
118	117	eqeq2d 2454	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
119		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
120	119	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
121	118, 120	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
122	121	anbi1d 704	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
123		reseq1 5109	. . . . . . . . . . . . . . . . . . . 20
124	123	eqeq2d 2454	. . . . . . . . . . . . . . . . . . 19
125		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20
126	125	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 19
127	124, 126	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
128	127	anbi2d 703	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
129	122, 128	rspc2ev 3086	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
130	100, 104, 116, 129	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	rexlimdva 2846	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	95, 132	impbid 191	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
134		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
135		mzpf 29077	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
136	134, 135	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
137		nn0ssz 10672	. . . . . . . . . . . . . . . . . . . . . 22
138		mapss 7260	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	3, 137, 138	mp2an 672	. . . . . . . . . . . . . . . . . . . . 21
140	139	sseli 3357	. . . . . . . . . . . . . . . . . . . 20
141		elmapssres 7242	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
142	140, 97, 141	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
143	142	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
144	136, 143	ffvelrnd 5849	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145	144	zred 10752	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
146		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
147		mzpf 29077	. . . . . . . . . . . . . . . . . . 19 mzPoly
148	146, 147	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
149		elmapssres 7242	. . . . . . . . . . . . . . . . . . . 20 $/\$
150	140, 101, 149	sylancl 662	. . . . . . . . . . . . . . . . . . 19
151	150	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	148, 151	ffvelrnd 5849	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153	152	zred 10752	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		sumsqeq0 11949	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
155	145, 153, 154	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
156	140	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		reseq1 5109	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
158	157	fveq2d 5700	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
159	158	oveq1d 6111	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
160		reseq1 5109	. . . . . . . . . . . . . . . . . . . . 21
161	160	fveq2d 5700	. . . . . . . . . . . . . . . . . . . 20
162	161	oveq1d 6111	. . . . . . . . . . . . . . . . . . 19
163	159, 162	oveq12d 6114	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		eqid 2443	. . . . . . . . . . . . . . . . . 18 $\$ $\$
165		ovex 6121	. . . . . . . . . . . . . . . . . 18 $\$
166	163, 164, 165	fvmpt 5779	. . . . . . . . . . . . . . . . 17 $\$ $\$
167	156, 166	syl 16	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	167	eqeq1d 2451	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
169	155, 168	bitr4d 256	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
170	169	anbi2d 703	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
171	170	rexbidva 2737	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
172	133, 171	bitrd 253	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	31, 172	syl5bbr 259	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	173	abbidv 2562	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
175	30, 174	syl5eq 2487	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
176		simpl 457	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
177		fzssuz 11504	. . . . . . . . . . . 12
178		uzssz 10885	. . . . . . . . . . . 12
179	177, 178	sstri 3370	. . . . . . . . . . 11
180	3, 179	pm3.2i 455	. . . . . . . . . 10 $/\$
181	180	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
182	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
183	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
184		simprl 755	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
185		mzpresrename 29092	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
186	182, 183, 184, 185	syl3anc 1218	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
187		2nn0 10601	. . . . . . . . . . 11
188		mzpexpmpt 29086	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
189	186, 187, 188	sylancl 662	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
190	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
191		simprr 756	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
192		mzpresrename 29092	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
193	182, 190, 191, 192	syl3anc 1218	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
194		mzpexpmpt 29086	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
195	193, 187, 194	sylancl 662	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
196		mzpaddmpt 29082	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
197	189, 195, 196	syl2anc 661	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
198		eldioph2 29105	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
199	176, 181, 197, 198	syl3anc 1218	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
200	175, 199	eqeltrd 2517	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
201		ineq12 3552	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
202	201	eleq1d 2509	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
203	200, 202	syl5ibrcom 222	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	203	rexlimdvva 2853	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
205	29, 204	syl5bir 218	. . . 4 mzPoly $\$ $\$ $/\$ $/\$