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 35615

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 35606	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10946	. . . . . . 7
4		difexg 4551	. . . . . . 7 $\$
5	3, 4	mp1i 13	. . . . . 6 $\$
6		ominf 7784	. . . . . . 7
7		nn0z 10960	. . . . . . . 8
8		lzenom 35612	. . . . . . . 8 $\$
9		enfi 7788	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 18	. . . . . . 7 $\$
11	6, 10	mtbiri 305	. . . . . 6 $\$
12		fz1eqin 35611	. . . . . . 7 $\$
13		inss1 3652	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3482	. . . . . 6 $\$
15		eldioph2b 35605	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1269	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10615	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10967	. . . . . . 7
20		nnuz 11194	. . . . . . . 8
21	20	uzinf 12179	. . . . . . 7
22	19, 21	mp1i 13	. . . . . 6
23		elfznn 11828	. . . . . . . 8
24	23	ssriv 3436	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 35605	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1269	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 717	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 2958	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3711	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 2958	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 770	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 771	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5105	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 736	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 774	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 772	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2491	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2488	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 35613	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1268	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3585	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10909	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10652	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 35610	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1268	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2497	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6306	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 736	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2531	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3577	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3589	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2499	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5119	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2503	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3578	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5101	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3625	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2497	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2491	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 35614	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1268	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2497	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 773	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2485	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 35614	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1268	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 775	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2485	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 538	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5099	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2461	. . . . . . . . . . . . . . . . . 18
84		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2453	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2453	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 717	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 717	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3150	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 436	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2886	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3560	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7496	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 668	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10957	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7496	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 668	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 764	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107	106	resabs1d 5134	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
108	105, 107	eqtr4d 2488	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109		simprrl 774	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110	108, 109	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
111		resabs1 5133	. . . . . . . . . . . . . . . . . . 19
112	24, 111	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
113	105, 112	eqtr4d 2488	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114		simprrr 775	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115	110, 113, 114	jca32 538	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
116		reseq1 5099	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
117	116	eqeq2d 2461	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
118		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
119	118	eqeq1d 2453	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
120	117, 119	anbi12d 717	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
121	120	anbi1d 711	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
122		reseq1 5099	. . . . . . . . . . . . . . . . . . . 20
123	122	eqeq2d 2461	. . . . . . . . . . . . . . . . . . 19
124		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20
125	124	eqeq1d 2453	. . . . . . . . . . . . . . . . . . 19
126	123, 125	anbi12d 717	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	126	anbi2d 710	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
128	121, 127	rspc2ev 3161	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
129	100, 104, 115, 128	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
130	129	ex 436	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	rexlimdva 2879	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	95, 131	impbid 194	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
133		simplrl 770	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
134		mzpf 35578	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
136		nn0ssz 10958	. . . . . . . . . . . . . . . . . . . . . 22
137		mapss 7514	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	3, 136, 137	mp2an 678	. . . . . . . . . . . . . . . . . . . . 21
139	138	sseli 3428	. . . . . . . . . . . . . . . . . . . 20
140		elmapssres 7496	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
141	139, 97, 140	sylancl 668	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
142	141	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
143	135, 142	ffvelrnd 6023	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
144	143	zred 11040	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145		simplrr 771	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
146		mzpf 35578	. . . . . . . . . . . . . . . . . . 19 mzPoly
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
148		elmapssres 7496	. . . . . . . . . . . . . . . . . . . 20 $/\$
149	139, 101, 148	sylancl 668	. . . . . . . . . . . . . . . . . . 19
150	149	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
151	147, 150	ffvelrnd 6023	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	151	zred 11040	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153		sumsqeq0 12353	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
154	144, 152, 153	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
155	139	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
156		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
157	156	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
158	157	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
159		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21
160	159	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20
161	160	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
162	158, 161	oveq12d 6308	. . . . . . . . . . . . . . . . . 18 $\$ $\$
163		eqid 2451	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		ovex 6318	. . . . . . . . . . . . . . . . . 18 $\$
165	162, 163, 164	fvmpt 5948	. . . . . . . . . . . . . . . . 17 $\$ $\$
166	155, 165	syl 17	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
167	166	eqeq1d 2453	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	154, 167	bitr4d 260	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
169	168	anbi2d 710	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
170	169	rexbidva 2898	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
171	132, 170	bitrd 257	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
172	31, 171	syl5bbr 263	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	172	abbidv 2569	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	30, 173	syl5eq 2497	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
175		simpl 459	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
176		fzssuz 11839	. . . . . . . . . . . 12
177		uzssz 11178	. . . . . . . . . . . 12
178	176, 177	sstri 3441	. . . . . . . . . . 11
179	3, 178	pm3.2i 457	. . . . . . . . . 10 $/\$
180	179	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
181	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
182	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
183		simprl 764	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
184		mzpresrename 35592	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
185	181, 182, 183, 184	syl3anc 1268	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
186		2nn0 10886	. . . . . . . . . . 11
187		mzpexpmpt 35587	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
188	185, 186, 187	sylancl 668	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
189	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
190		simprr 766	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
191		mzpresrename 35592	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
192	181, 189, 190, 191	syl3anc 1268	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
193		mzpexpmpt 35587	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
194	192, 186, 193	sylancl 668	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
195		mzpaddmpt 35583	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
196	188, 194, 195	syl2anc 667	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
197		eldioph2 35604	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
198	175, 180, 196, 197	syl3anc 1268	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
199	174, 198	eqeltrd 2529	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
200		ineq12 3629	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
201	200	eleq1d 2513	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
202	199, 201	syl5ibrcom 226	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
203	202	rexlimdvva 2886	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	29, 203	syl5bir 222	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$ Dioph
205	28, 204	sylbid 219	. . 3