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 30310

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 30301	. . 3 Dioph
2		id 22	. . . . . 6
3		zex 10869	. . . . . . 7
4		difexg 4595	. . . . . . 7 $\$
5	3, 4	mp1i 12	. . . . . 6 $\$
6		ominf 7729	. . . . . . 7
7		nn0z 10883	. . . . . . . 8
8		lzenom 30307	. . . . . . . 8 $\$
9		enfi 7733	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 20	. . . . . . 7 $\$
11	6, 10	mtbiri 303	. . . . . 6 $\$
12		fz1eqin 30306	. . . . . . 7 $\$
13		inss1 3718	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3554	. . . . . 6 $\$
15		eldioph2b 30300	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1229	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 10538	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10890	. . . . . . 7
20		nnuz 11113	. . . . . . . 8
21	20	uzinf 12040	. . . . . . 7
22	19, 21	mp1i 12	. . . . . 6
23		elfznn 11710	. . . . . . . 8
24	23	ssriv 3508	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 30300	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1229	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 710	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 3029	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3766	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 3029	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 759	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 760	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5271	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5271	. . . . . . . . . . . . . . . . . . . . 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 2514	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2511	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 30308	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3655	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10831	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 10574	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 30305	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2520	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6298	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2557	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3647	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3659	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2522	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5286	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2526	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3648	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5267	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3691	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2520	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5271	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5271	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2514	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2511	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 30309	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2520	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5868	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 762	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 30309	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5868	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 764	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 535	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5265	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18
84		reseq1 5265	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5868	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2469	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5265	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5868	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2469	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3214	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2962	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3631	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 7440	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10880	. . . . . . . . . . . . . . . . . 18
102		elmapssres 7440	. . . . . . . . . . . . . . . . . 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 5300	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
108	106, 107	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	105, 108	eqtr4d 2511	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110		simprrl 763	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111	109, 110	jca 532	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
112		resabs1 5300	. . . . . . . . . . . . . . . . . . 19
113	24, 112	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114	105, 113	eqtr4d 2511	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115		simprrr 764	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116	111, 114, 115	jca32 535	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
117		reseq1 5265	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
118	117	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
119		fveq2 5864	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
120	119	eqeq1d 2469	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
121	118, 120	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
122	121	anbi1d 704	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
123		reseq1 5265	. . . . . . . . . . . . . . . . . . . 20
124	123	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
125		fveq2 5864	. . . . . . . . . . . . . . . . . . . 20
126	125	eqeq1d 2469	. . . . . . . . . . . . . . . . . . 19
127	124, 126	anbi12d 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
128	127	anbi2d 703	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
129	122, 128	rspc2ev 3225	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
130	100, 104, 116, 129	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	ex 434	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	rexlimdva 2955	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	95, 132	impbid 191	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
134		simplrl 759	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
135		mzpf 30272	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
136	134, 135	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
137		nn0ssz 10881	. . . . . . . . . . . . . . . . . . . . . 22
138		mapss 7458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	3, 137, 138	mp2an 672	. . . . . . . . . . . . . . . . . . . . 21
140	139	sseli 3500	. . . . . . . . . . . . . . . . . . . 20
141		elmapssres 7440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
142	140, 97, 141	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
143	142	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
144	136, 143	ffvelrnd 6020	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145	144	zred 10962	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
146		simplrr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
147		mzpf 30272	. . . . . . . . . . . . . . . . . . 19 mzPoly
148	146, 147	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
149		elmapssres 7440	. . . . . . . . . . . . . . . . . . . 20 $/\$
150	140, 101, 149	sylancl 662	. . . . . . . . . . . . . . . . . . 19
151	150	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	148, 151	ffvelrnd 6020	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153	152	zred 10962	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		sumsqeq0 12210	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
155	145, 153, 154	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
156	140	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		reseq1 5265	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
158	157	fveq2d 5868	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
159	158	oveq1d 6297	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
160		reseq1 5265	. . . . . . . . . . . . . . . . . . . . 21
161	160	fveq2d 5868	. . . . . . . . . . . . . . . . . . . 20
162	161	oveq1d 6297	. . . . . . . . . . . . . . . . . . 19
163	159, 162	oveq12d 6300	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		eqid 2467	. . . . . . . . . . . . . . . . . 18 $\$ $\$
165		ovex 6307	. . . . . . . . . . . . . . . . . 18 $\$
166	163, 164, 165	fvmpt 5948	. . . . . . . . . . . . . . . . 17 $\$ $\$
167	156, 166	syl 16	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	167	eqeq1d 2469	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
169	155, 168	bitr4d 256	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
170	169	anbi2d 703	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
171	170	rexbidva 2970	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
172	133, 171	bitrd 253	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	31, 172	syl5bbr 259	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	173	abbidv 2603	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
175	30, 174	syl5eq 2520	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
176		simpl 457	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
177		fzssuz 11720	. . . . . . . . . . . 12
178		uzssz 11097	. . . . . . . . . . . 12
179	177, 178	sstri 3513	. . . . . . . . . . 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 30287	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
186	182, 183, 184, 185	syl3anc 1228	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
187		2nn0 10808	. . . . . . . . . . 11
188		mzpexpmpt 30281	. . . . . . . . . . 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 30287	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
193	182, 190, 191, 192	syl3anc 1228	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
194		mzpexpmpt 30281	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
195	193, 187, 194	sylancl 662	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
196		mzpaddmpt 30277	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
197	189, 195, 196	syl2anc 661	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
198		eldioph2 30299	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
199	176, 181, 197, 198	syl3anc 1228	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
200	175, 199	eqeltrd 2555	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
201		ineq12 3695	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
202	201	eleq1d 2536	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
203	200, 202	syl5ibrcom 222	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	203	rexlimdvva 2962	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
205	29, 204	syl5bir 218	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ mzPoly