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 30945

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 30936	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10869	. . . . . . 7
4		difexg 4585	. . . . . . 7 $\$
5	3, 4	mp1i 12	. . . . . 6 $\$
6		ominf 7725	. . . . . . 7
7		nn0z 10883	. . . . . . . 8
8		lzenom 30942	. . . . . . . 8 $\$
9		enfi 7729	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 20	. . . . . . 7 $\$
11	6, 10	mtbiri 301	. . . . . 6 $\$
12		fz1eqin 30941	. . . . . . 7 $\$
13		inss1 3704	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3539	. . . . . 6 $\$
15		eldioph2b 30935	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1227	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10537	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10890	. . . . . . 7
20		nnuz 11117	. . . . . . . 8
21	20	uzinf 12058	. . . . . . 7
22	19, 21	mp1i 12	. . . . . 6
23		elfznn 11717	. . . . . . . 8
24	23	ssriv 3493	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 30935	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1227	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 708	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 3022	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3763	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 3022	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 760	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5262	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5262	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 761	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2501	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2498	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 30943	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1226	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3641	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10831	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10574	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 30940	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1226	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2507	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6286	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2544	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3633	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3645	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2509	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5276	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2513	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3634	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5258	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3677	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2507	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5262	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5262	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2501	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2498	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 30944	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1226	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2507	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5852	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 762	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2495	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 30944	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1226	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5852	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 764	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2495	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 533	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5256	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2468	. . . . . . . . . . . . . . . . . 18
84		reseq1 5256	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2456	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5256	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2456	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 708	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 708	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3207	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 432	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2953	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 459	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3617	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7436	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 660	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10880	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7436	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 660	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 754	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107	106	resabs1d 5291	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
108	105, 107	eqtr4d 2498	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109		simprrl 763	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110	108, 109	jca 530	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
111		resabs1 5290	. . . . . . . . . . . . . . . . . . 19
112	24, 111	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
113	105, 112	eqtr4d 2498	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114		simprrr 764	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115	110, 113, 114	jca32 533	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
116		reseq1 5256	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
117	116	eqeq2d 2468	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
118		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
119	118	eqeq1d 2456	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
120	117, 119	anbi12d 708	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
121	120	anbi1d 702	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
122		reseq1 5256	. . . . . . . . . . . . . . . . . . . 20
123	122	eqeq2d 2468	. . . . . . . . . . . . . . . . . . 19
124		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20
125	124	eqeq1d 2456	. . . . . . . . . . . . . . . . . . 19
126	123, 125	anbi12d 708	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	126	anbi2d 701	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
128	121, 127	rspc2ev 3218	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
129	100, 104, 115, 128	syl3anc 1226	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
130	129	ex 432	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	rexlimdva 2946	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	95, 131	impbid 191	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
133		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
134		mzpf 30908	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
135	133, 134	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
136		nn0ssz 10881	. . . . . . . . . . . . . . . . . . . . . 22
137		mapss 7454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	3, 136, 137	mp2an 670	. . . . . . . . . . . . . . . . . . . . 21
139	138	sseli 3485	. . . . . . . . . . . . . . . . . . . 20
140		elmapssres 7436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
141	139, 97, 140	sylancl 660	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
142	141	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
143	135, 142	ffvelrnd 6008	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
144	143	zred 10965	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
146		mzpf 30908	. . . . . . . . . . . . . . . . . . 19 mzPoly
147	145, 146	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
148		elmapssres 7436	. . . . . . . . . . . . . . . . . . . 20 $/\$
149	139, 101, 148	sylancl 660	. . . . . . . . . . . . . . . . . . 19
150	149	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
151	147, 150	ffvelrnd 6008	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	151	zred 10965	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153		sumsqeq0 12228	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
154	144, 152, 153	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
155	139	adantl 464	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
156		reseq1 5256	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
157	156	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
158	157	oveq1d 6285	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
159		reseq1 5256	. . . . . . . . . . . . . . . . . . . . 21
160	159	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20
161	160	oveq1d 6285	. . . . . . . . . . . . . . . . . . 19
162	158, 161	oveq12d 6288	. . . . . . . . . . . . . . . . . 18 $\$ $\$
163		eqid 2454	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		ovex 6298	. . . . . . . . . . . . . . . . . 18 $\$
165	162, 163, 164	fvmpt 5931	. . . . . . . . . . . . . . . . 17 $\$ $\$
166	155, 165	syl 16	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
167	166	eqeq1d 2456	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	154, 167	bitr4d 256	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
169	168	anbi2d 701	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
170	169	rexbidva 2962	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
171	132, 170	bitrd 253	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
172	31, 171	syl5bbr 259	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	172	abbidv 2590	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	30, 173	syl5eq 2507	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
175		simpl 455	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
176		fzssuz 11728	. . . . . . . . . . . 12
177		uzssz 11101	. . . . . . . . . . . 12
178	176, 177	sstri 3498	. . . . . . . . . . 11
179	3, 178	pm3.2i 453	. . . . . . . . . 10 $/\$
180	179	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
181	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
182	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
183		simprl 754	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
184		mzpresrename 30922	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
185	181, 182, 183, 184	syl3anc 1226	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
186		2nn0 10808	. . . . . . . . . . 11
187		mzpexpmpt 30917	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
188	185, 186, 187	sylancl 660	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
189	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
190		simprr 755	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
191		mzpresrename 30922	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
192	181, 189, 190, 191	syl3anc 1226	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
193		mzpexpmpt 30917	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
194	192, 186, 193	sylancl 660	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
195		mzpaddmpt 30913	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
196	188, 194, 195	syl2anc 659	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
197		eldioph2 30934	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
198	175, 180, 196, 197	syl3anc 1226	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
199	174, 198	eqeltrd 2542	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
200		ineq12 3681	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
201	200	eleq1d 2523	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
202	199, 201	syl5ibrcom 222	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
203	202	rexlimdvva 2953	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	29, 203	syl5bir 218	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$ Dioph
205	28, 204	sylbid 215	. . 3