diophin - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > diophin		Unicode version

Theorem diophin 26721

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 26712	. . 3 Dioph
2		id 20	. . . . . 6
3		zex 10247	. . . . . . 7
4		difexg 4311	. . . . . . 7 $\$
5	3, 4	mp1i 12	. . . . . 6 $\$
6		ominf 7280	. . . . . . 7
7		nn0z 10260	. . . . . . . 8
8		lzenom 26718	. . . . . . . 8 $\$
9		enfi 7284	. . . . . . . 8 $\$ $\$
10	7, 8, 9	3syl 19	. . . . . . 7 $\$
11	6, 10	mtbiri 295	. . . . . 6 $\$
12		fz1eqin 26717	. . . . . . 7 $\$
13		inss1 3521	. . . . . . 7 $\$ $\$
14	12, 13	syl6eqss 3358	. . . . . 6 $\$
15		eldioph2b 26711	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ Dioph mzPoly $\$ $\$ $/\$
16	2, 5, 11, 14, 15	syl22anc 1185	. . . . 5 Dioph mzPoly $\$ $\$ $/\$
17		nnex 9962	. . . . . . 7
18	17	a1i 11	. . . . . 6
19		1z 10267	. . . . . . 7
20		nnuz 10477	. . . . . . . 8
21	20	uzinf 11260	. . . . . . 7
22	19, 21	mp1i 12	. . . . . 6
23		elfznn 11036	. . . . . . . 8
24	23	ssriv 3312	. . . . . . 7
25	24	a1i 11	. . . . . 6
26		eldioph2b 26711	. . . . . 6 $/\$ $/\$ $/\$ Dioph mzPoly $/\$
27	2, 18, 22, 25, 26	syl22anc 1185	. . . . 5 Dioph mzPoly $/\$
28	16, 27	anbi12d 692	. . . 4 Dioph $/\$ Dioph mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
29		reeanv 2835	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ mzPoly $\$ $\$ $/\$ $/\$ mzPoly $/\$
30		inab 3569	. . . . . . . . 9 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		reeanv 2835	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
32		simplrl 737	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
33		simplrr 738	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	12	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . 21 $\$
35	34	reseq2d 5105	. . . . . . . . . . . . . . . . . . . 20 $\$
36	35	ad3antrrr 711	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
37	34	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . 21 $\$
38	37	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		simprrl 741	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprll 739	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	38, 39, 40	3eqtr2d 2442	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
42	36, 41	eqtr4d 2439	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
43		elmapresaun 26719	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\$ $\$ $\$
44	32, 33, 42, 43	syl3anc 1184	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45	20	uneq2i 3458	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
47		nn0p1nn 10215	. . . . . . . . . . . . . . . . . . . . . 22
48	47	nnge1d 9998	. . . . . . . . . . . . . . . . . . . . 21
49		lzunuz 26716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
50	7, 46, 48, 49	syl3anc 1184	. . . . . . . . . . . . . . . . . . . 20 $\$
51	45, 50	syl5eq 2448	. . . . . . . . . . . . . . . . . . 19 $\$
52	51	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 $\$
53	52	ad3antrrr 711	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	44, 53	eleqtrd 2480	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		unidm 3450	. . . . . . . . . . . . . . . . . . 19
56	40, 39	uneq12d 3462	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 56	syl5eqr 2450	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		resundir 5120	. . . . . . . . . . . . . . . . . 18
59	57, 58	syl6eqr 2454	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		uncom 3451	. . . . . . . . . . . . . . . . . . . . 21
61	60	reseq1i 5101	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
62		incom 3493	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
63	62, 34	syl5eq 2448	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
64	63	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
65	64	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
66	63	reseq2d 5105	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
67	66	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
68	67, 40, 39	3eqtr2d 2442	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
69	65, 68	eqtr4d 2439	. . . . . . . . . . . . . . . . . . . . 21 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
70		elmapresaunres2 26720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$ $\$ $\$ $\$
71	33, 32, 69, 70	syl3anc 1184	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
72	61, 71	syl5eq 2448	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	fveq2d 5691	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
74		simprlr 740	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	73, 74	eqtrd 2436	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
76		elmapresaunres2 26720	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$ $\$
77	32, 33, 42, 76	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	fveq2d 5691	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprrr 742	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	78, 79	eqtrd 2436	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	59, 75, 80	jca32 522	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
82		reseq1 5099	. . . . . . . . . . . . . . . . . . 19
83	82	eqeq2d 2415	. . . . . . . . . . . . . . . . . 18
84		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
85	84	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
86	85	eqeq1d 2412	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
87		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21
88	87	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20
89	88	eqeq1d 2412	. . . . . . . . . . . . . . . . . . 19
90	86, 89	anbi12d 692	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$
91	83, 90	anbi12d 692	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\$ $/\$
92	91	rspcev 3012	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
93	54, 81, 92	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
94	93	ex 424	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
95	94	rexlimdvva 2797	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
96		simpr 448	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
97		difss 3434	. . . . . . . . . . . . . . . . . 18 $\$
98		elmapssres 26661	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
99	96, 97, 98	sylancl 644	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
100	99	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
101		nnssz 10257	. . . . . . . . . . . . . . . . . 18
102		elmapssres 26661	. . . . . . . . . . . . . . . . . 18 $/\$
103	96, 101, 102	sylancl 644	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
104	103	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
105		simprl 733	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
106	14	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . 20 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		resabs1 5134	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
108	106, 107	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	105, 108	eqtr4d 2439	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
110		simprrl 741	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$
111	109, 110	jca 519	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
112		resabs1 5134	. . . . . . . . . . . . . . . . . . 19
113	24, 112	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
114	105, 113	eqtr4d 2439	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
115		simprrr 742	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$
116	111, 114, 115	jca32 522	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
117		reseq1 5099	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
118	117	eqeq2d 2415	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
119		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
120	119	eqeq1d 2412	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
121	118, 120	anbi12d 692	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$
122	121	anbi1d 686	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
123		reseq1 5099	. . . . . . . . . . . . . . . . . . . 20
124	123	eqeq2d 2415	. . . . . . . . . . . . . . . . . . 19
125		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20
126	125	eqeq1d 2412	. . . . . . . . . . . . . . . . . . 19
127	124, 126	anbi12d 692	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
128	127	anbi2d 685	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
129	122, 128	rspc2ev 3020	. . . . . . . . . . . . . . . 16 $\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
130	100, 104, 116, 129	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
131	130	ex 424	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
132	131	rexlimdva 2790	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
133	95, 132	impbid 184	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
134		simplrl 737	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly $\$
135		mzpf 26683	. . . . . . . . . . . . . . . . . . 19 mzPoly $\$ $\$
136	134, 135	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
137		nn0ssz 10258	. . . . . . . . . . . . . . . . . . . . . 22
138		mapss 7015	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	3, 137, 138	mp2an 654	. . . . . . . . . . . . . . . . . . . . 21
140	139	sseli 3304	. . . . . . . . . . . . . . . . . . . 20
141		elmapssres 26661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
142	140, 97, 141	sylancl 644	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
143	142	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
144	136, 143	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
145	144	zred 10331	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$
146		simplrr 738	. . . . . . . . . . . . . . . . . . 19 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ mzPoly
147		mzpf 26683	. . . . . . . . . . . . . . . . . . 19 mzPoly
148	146, 147	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
149		elmapssres 26661	. . . . . . . . . . . . . . . . . . . 20 $/\$
150	140, 101, 149	sylancl 644	. . . . . . . . . . . . . . . . . . 19
151	150	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
152	148, 151	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
153	152	zred 10331	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
154		sumsqeq0 11415	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $/\$ $\$
155	145, 153, 154	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
156	140	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
157		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
158	157	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
159	158	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
160		reseq1 5099	. . . . . . . . . . . . . . . . . . . . 21
161	160	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20
162	161	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19
163	159, 162	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 $\$ $\$
164		eqid 2404	. . . . . . . . . . . . . . . . . 18 $\$ $\$
165		ovex 6065	. . . . . . . . . . . . . . . . . 18 $\$
166	163, 164, 165	fvmpt 5765	. . . . . . . . . . . . . . . . 17 $\$ $\$
167	156, 166	syl 16	. . . . . . . . . . . . . . . 16 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
168	167	eqeq1d 2412	. . . . . . . . . . . . . . 15 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $\$
169	155, 168	bitr4d 248	. . . . . . . . . . . . . 14 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $\$
170	169	anbi2d 685	. . . . . . . . . . . . 13 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $/\$ $\$ $/\$ $/\$ $\$
171	170	rexbidva 2683	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ $/\$ $/\$ $\$
172	133, 171	bitrd 245	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
173	31, 172	syl5bbr 251	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
174	173	abbidv 2518	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $/\$ $\$
175	30, 174	syl5eq 2448	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ $\$
176		simpl 444	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly
177		fzssuz 11049	. . . . . . . . . . . 12
178		uzssz 10461	. . . . . . . . . . . 12
179	177, 178	sstri 3317	. . . . . . . . . . 11
180	3, 179	pm3.2i 442	. . . . . . . . . 10 $/\$
181	180	a1i 11	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $/\$
182	3	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
183	97	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly $\$
184		simprl 733	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly $\$
185		mzpresrename 26697	. . . . . . . . . . . 12 $/\$ $\$ $/\$ mzPoly $\$ $\$ mzPoly
186	182, 183, 184, 185	syl3anc 1184	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
187		2nn0 10194	. . . . . . . . . . 11
188		mzpexpmpt 26692	. . . . . . . . . . 11 $\$ mzPoly $/\$ $\$ mzPoly
189	186, 187, 188	sylancl 644	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
190	101	a1i 11	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly
191		simprr 734	. . . . . . . . . . . 12 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
192		mzpresrename 26697	. . . . . . . . . . . 12 $/\$ $/\$ mzPoly mzPoly
193	182, 190, 191, 192	syl3anc 1184	. . . . . . . . . . 11 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
194		mzpexpmpt 26692	. . . . . . . . . . 11 mzPoly $/\$ mzPoly
195	193, 187, 194	sylancl 644	. . . . . . . . . 10 $/\$ mzPoly $\$ $/\$ mzPoly mzPoly
196		mzpaddmpt 26688	. . . . . . . . . 10 $\$ mzPoly $/\$ mzPoly $\$ mzPoly
197	189, 195, 196	syl2anc 643	. . . . . . . . 9 $/\$ mzPoly $\$ $/\$ mzPoly $\$ mzPoly
198		eldioph2 26710	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ mzPoly $/\$ $\$ Dioph
199	176, 181, 197, 198	syl3anc 1184	. . . . . . . 8 $/\$ mzPoly $\$ $/\$ mzPoly $/\$ $\$ Dioph
200	175, 199	eqeltrd 2478	. . . . . . 7 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ Dioph
201		ineq12 3497	. . . . . . . 8 $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
202	201	eleq1d 2470	. . . . . . 7 $\$ $/\$ $/\$ $/\$ Dioph $\$ $/\$ $/\$ Dioph
203	200, 202	syl5ibrcom 214	. . . . . 6 $/\$ mzPoly $\$ $/\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
204	203	rexlimdvva 2797	. . . . 5 mzPoly $\$ mzPoly $\$ $/\$ $/\$ $/\$ Dioph
205	29, 204	syl5bir 210	. . . 4 mzPoly $\$ $\$ $/\$ $/\$ mzPoly