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 29036

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 29027	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10651	. . . . . . 7
4		difexg 4437	. . . . . . 7 $\$
5	3, 4	mp1i 12	. . . . . 6 $\$
6		ominf 7521	. . . . . . 7
7		nn0z 10665	. . . . . . . 8
8		lzenom 29033	. . . . . . . 8 $\$
9		enfi 7525	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 20	. . . . . . 7 $\$
11	6, 10	mtbiri 303	. . . . . 6 $\$
12		fz1eqin 29032	. . . . . . 7 $\$
13		inss1 3567	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3403	. . . . . 6 $\$
15		eldioph2b 29026	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1214	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10324	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10672	. . . . . . 7
20		nnuz 10892	. . . . . . . 8
21	20	uzinf 11784	. . . . . . 7
22	19, 21	mp1i 12	. . . . . 6
23		elfznn 11474	. . . . . . . 8
24	23	ssriv 3357	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 29026	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1214	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 705	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 2886	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3615	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 2886	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 754	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 755	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2446	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5106	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 724	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5106	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 758	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2479	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2476	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 29034	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1213	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3504	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10615	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10360	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 29031	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1213	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2485	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6106	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 724	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2517	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3496	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3508	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2487	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5122	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2491	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3497	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5102	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3540	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2485	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5106	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5106	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2479	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 29035	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1213	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2485	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5692	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 757	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2473	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 29035	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1213	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5692	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 759	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2473	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 532	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5100	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2452	. . . . . . . . . . . . . . . . . 18
84		reseq1 5100	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2449	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5100	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2449	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 705	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 705	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3070	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 656	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2846	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 458	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3480	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7233	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 657	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10662	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7233	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 657	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 750	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		resabs1 5136	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
108	106, 107	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	105, 108	eqtr4d 2476	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110		simprrl 758	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111	109, 110	jca 529	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
112		resabs1 5136	. . . . . . . . . . . . . . . . . . 19
113	24, 112	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114	105, 113	eqtr4d 2476	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115		simprrr 759	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116	111, 114, 115	jca32 532	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
117		reseq1 5100	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
118	117	eqeq2d 2452	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
119		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
120	119	eqeq1d 2449	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
121	118, 120	anbi12d 705	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
122	121	anbi1d 699	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
123		reseq1 5100	. . . . . . . . . . . . . . . . . . . 20
124	123	eqeq2d 2452	. . . . . . . . . . . . . . . . . . 19
125		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20
126	125	eqeq1d 2449	. . . . . . . . . . . . . . . . . . 19
127	124, 126	anbi12d 705	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
128	127	anbi2d 698	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
129	122, 128	rspc2ev 3078	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
130	100, 104, 116, 129	syl3anc 1213	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	rexlimdva 2839	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	95, 132	impbid 191	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
134		simplrl 754	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
135		mzpf 28997	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
136	134, 135	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
137		nn0ssz 10663	. . . . . . . . . . . . . . . . . . . . . 22
138		mapss 7251	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	3, 137, 138	mp2an 667	. . . . . . . . . . . . . . . . . . . . 21
140	139	sseli 3349	. . . . . . . . . . . . . . . . . . . 20
141		elmapssres 7233	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
142	140, 97, 141	sylancl 657	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
143	142	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
144	136, 143	ffvelrnd 5841	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145	144	zred 10743	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
146		simplrr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
147		mzpf 28997	. . . . . . . . . . . . . . . . . . 19 mzPoly
148	146, 147	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
149		elmapssres 7233	. . . . . . . . . . . . . . . . . . . 20 $/\$
150	140, 101, 149	sylancl 657	. . . . . . . . . . . . . . . . . . 19
151	150	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	148, 151	ffvelrnd 5841	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153	152	zred 10743	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		sumsqeq0 11940	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
155	145, 153, 154	syl2anc 656	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
156	140	adantl 463	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		reseq1 5100	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
158	157	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
159	158	oveq1d 6105	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
160		reseq1 5100	. . . . . . . . . . . . . . . . . . . . 21
161	160	fveq2d 5692	. . . . . . . . . . . . . . . . . . . 20
162	161	oveq1d 6105	. . . . . . . . . . . . . . . . . . 19
163	159, 162	oveq12d 6108	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		eqid 2441	. . . . . . . . . . . . . . . . . 18 $\$ $\$
165		ovex 6115	. . . . . . . . . . . . . . . . . 18 $\$
166	163, 164, 165	fvmpt 5771	. . . . . . . . . . . . . . . . 17 $\$ $\$
167	156, 166	syl 16	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	167	eqeq1d 2449	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
169	155, 168	bitr4d 256	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
170	169	anbi2d 698	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
171	170	rexbidva 2730	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
172	133, 171	bitrd 253	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	31, 172	syl5bbr 259	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	173	abbidv 2555	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
175	30, 174	syl5eq 2485	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
176		simpl 454	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
177		fzssuz 11495	. . . . . . . . . . . 12
178		uzssz 10876	. . . . . . . . . . . 12
179	177, 178	sstri 3362	. . . . . . . . . . 11
180	3, 179	pm3.2i 452	. . . . . . . . . 10 $/\$
181	180	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
182	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
183	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
184		simprl 750	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
185		mzpresrename 29012	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
186	182, 183, 184, 185	syl3anc 1213	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
187		2nn0 10592	. . . . . . . . . . 11
188		mzpexpmpt 29006	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
189	186, 187, 188	sylancl 657	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
190	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
191		simprr 751	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
192		mzpresrename 29012	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
193	182, 190, 191, 192	syl3anc 1213	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
194		mzpexpmpt 29006	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
195	193, 187, 194	sylancl 657	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
196		mzpaddmpt 29002	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
197	189, 195, 196	syl2anc 656	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
198		eldioph2 29025	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
199	176, 181, 197, 198	syl3anc 1213	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
200	175, 199	eqeltrd 2515	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
201		ineq12 3544	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
202	201	eleq1d 2507	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
203	200, 202	syl5ibrcom 222	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	203	rexlimdvva 2846	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
205	29, 204	syl5bir 218	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ <