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

Theorem diophin 26833
 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.
StepHypRef Expression
1 eldiophelnn0 26824 . . 3 Dioph
2 id 21 . . . . . 6
3 zex 10293 . . . . . . 7
4 difexg 4353 . . . . . . 7
53, 4mp1i 12 . . . . . 6
6 ominf 7323 . . . . . . 7
7 nn0z 10306 . . . . . . . 8
8 lzenom 26830 . . . . . . . 8
9 enfi 7327 . . . . . . . 8
107, 8, 93syl 19 . . . . . . 7
116, 10mtbiri 296 . . . . . 6
12 fz1eqin 26829 . . . . . . 7
13 inss1 3563 . . . . . . 7
1412, 13syl6eqss 3400 . . . . . 6
15 eldioph2b 26823 . . . . . 6 Dioph mzPoly
162, 5, 11, 14, 15syl22anc 1186 . . . . 5 Dioph mzPoly
17 nnex 10008 . . . . . . 7
1817a1i 11 . . . . . 6
19 1z 10313 . . . . . . 7
20 nnuz 10523 . . . . . . . 8
2120uzinf 11307 . . . . . . 7
2219, 21mp1i 12 . . . . . 6
23 elfznn 11082 . . . . . . . 8
2423ssriv 3354 . . . . . . 7
2524a1i 11 . . . . . 6
26 eldioph2b 26823 . . . . . 6 Dioph mzPoly
272, 18, 22, 25, 26syl22anc 1186 . . . . 5 Dioph mzPoly
2816, 27anbi12d 693 . . . 4 Dioph Dioph mzPoly mzPoly
29 reeanv 2877 . . . . 5 mzPoly mzPoly mzPoly mzPoly
30 inab 3611 . . . . . . . . 9
31 reeanv 2877 . . . . . . . . . . 11
32 simplrl 738 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
33 simplrr 739 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
3412eqcomd 2443 . . . . . . . . . . . . . . . . . . . . 21
3534reseq2d 5148 . . . . . . . . . . . . . . . . . . . 20
3635ad3antrrr 712 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
3734reseq2d 5148 . . . . . . . . . . . . . . . . . . . . 21
3837ad3antrrr 712 . . . . . . . . . . . . . . . . . . . 20 mzPoly mzPoly
39 simprrl 742 . . . . . . . . . . . . . . . . . . . 20 mzPoly mzPoly
40 simprll 740 . . . . . . . . . . . . . . . . . . . 20 mzPoly mzPoly
4138, 39, 403eqtr2d 2476 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
4236, 41eqtr4d 2473 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
43 elmapresaun 26831 . . . . . . . . . . . . . . . . . 18
4432, 33, 42, 43syl3anc 1185 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
4520uneq2i 3500 . . . . . . . . . . . . . . . . . . . 20
4619a1i 11 . . . . . . . . . . . . . . . . . . . . 21
47 nn0p1nn 10261 . . . . . . . . . . . . . . . . . . . . . 22
4847nnge1d 10044 . . . . . . . . . . . . . . . . . . . . 21
49 lzunuz 26828 . . . . . . . . . . . . . . . . . . . . 21
507, 46, 48, 49syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20
5145, 50syl5eq 2482 . . . . . . . . . . . . . . . . . . 19
5251oveq2d 6099 . . . . . . . . . . . . . . . . . 18
5352ad3antrrr 712 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
5444, 53eleqtrd 2514 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
55 unidm 3492 . . . . . . . . . . . . . . . . . . 19
5640, 39uneq12d 3504 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
5755, 56syl5eqr 2484 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
58 resundir 5163 . . . . . . . . . . . . . . . . . 18
5957, 58syl6eqr 2488 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
60 uncom 3493 . . . . . . . . . . . . . . . . . . . . 21
6160reseq1i 5144 . . . . . . . . . . . . . . . . . . . 20
62 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . . 25
6362, 34syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . 24
6463reseq2d 5148 . . . . . . . . . . . . . . . . . . . . . . 23
6564ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . 22 mzPoly mzPoly
6663reseq2d 5148 . . . . . . . . . . . . . . . . . . . . . . . 24
6766ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . 23 mzPoly mzPoly
6867, 40, 393eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . . 22 mzPoly mzPoly
6965, 68eqtr4d 2473 . . . . . . . . . . . . . . . . . . . . 21 mzPoly mzPoly
70 elmapresaunres2 26832 . . . . . . . . . . . . . . . . . . . . 21
7133, 32, 69, 70syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20 mzPoly mzPoly
7261, 71syl5eq 2482 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
7372fveq2d 5734 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
74 simprlr 741 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
7573, 74eqtrd 2470 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
76 elmapresaunres2 26832 . . . . . . . . . . . . . . . . . . . 20
7732, 33, 42, 76syl3anc 1185 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
7877fveq2d 5734 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
79 simprrr 743 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
8078, 79eqtrd 2470 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
8159, 75, 80jca32 523 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
82 reseq1 5142 . . . . . . . . . . . . . . . . . . 19
8382eqeq2d 2449 . . . . . . . . . . . . . . . . . 18
84 reseq1 5142 . . . . . . . . . . . . . . . . . . . . 21
8584fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20
8685eqeq1d 2446 . . . . . . . . . . . . . . . . . . 19
87 reseq1 5142 . . . . . . . . . . . . . . . . . . . . 21
8887fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20
8988eqeq1d 2446 . . . . . . . . . . . . . . . . . . 19
9086, 89anbi12d 693 . . . . . . . . . . . . . . . . . 18
9183, 90anbi12d 693 . . . . . . . . . . . . . . . . 17
9291rspcev 3054 . . . . . . . . . . . . . . . 16
9354, 81, 92syl2anc 644 . . . . . . . . . . . . . . 15 mzPoly mzPoly
9493ex 425 . . . . . . . . . . . . . 14 mzPoly mzPoly
9594rexlimdvva 2839 . . . . . . . . . . . . 13 mzPoly mzPoly
96 simpr 449 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
97 difss 3476 . . . . . . . . . . . . . . . . . 18
98 elmapssres 26773 . . . . . . . . . . . . . . . . . 18
9996, 97, 98sylancl 645 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
10099adantr 453 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
101 nnssz 10303 . . . . . . . . . . . . . . . . . 18
102 elmapssres 26773 . . . . . . . . . . . . . . . . . 18
10396, 101, 102sylancl 645 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
104103adantr 453 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
105 simprl 734 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
10614ad3antrrr 712 . . . . . . . . . . . . . . . . . . . 20 mzPoly mzPoly
107 resabs1 5177 . . . . . . . . . . . . . . . . . . . 20
108106, 107syl 16 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly
109105, 108eqtr4d 2473 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
110 simprrl 742 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
111109, 110jca 520 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
112 resabs1 5177 . . . . . . . . . . . . . . . . . . 19
11324, 112mp1i 12 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
114105, 113eqtr4d 2473 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
115 simprrr 743 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
116111, 114, 115jca32 523 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
117 reseq1 5142 . . . . . . . . . . . . . . . . . . . 20
118117eqeq2d 2449 . . . . . . . . . . . . . . . . . . 19
119 fveq2 5730 . . . . . . . . . . . . . . . . . . . 20
120119eqeq1d 2446 . . . . . . . . . . . . . . . . . . 19
121118, 120anbi12d 693 . . . . . . . . . . . . . . . . . 18
122121anbi1d 687 . . . . . . . . . . . . . . . . 17
123 reseq1 5142 . . . . . . . . . . . . . . . . . . . 20
124123eqeq2d 2449 . . . . . . . . . . . . . . . . . . 19
125 fveq2 5730 . . . . . . . . . . . . . . . . . . . 20
126125eqeq1d 2446 . . . . . . . . . . . . . . . . . . 19
127124, 126anbi12d 693 . . . . . . . . . . . . . . . . . 18
128127anbi2d 686 . . . . . . . . . . . . . . . . 17
129122, 128rspc2ev 3062 . . . . . . . . . . . . . . . 16
130100, 104, 116, 129syl3anc 1185 . . . . . . . . . . . . . . 15 mzPoly mzPoly
131130ex 425 . . . . . . . . . . . . . 14 mzPoly mzPoly
132131rexlimdva 2832 . . . . . . . . . . . . 13 mzPoly mzPoly
13395, 132impbid 185 . . . . . . . . . . . 12 mzPoly mzPoly
134 simplrl 738 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly mzPoly
135 mzpf 26795 . . . . . . . . . . . . . . . . . . 19 mzPoly
136134, 135syl 16 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
137 nn0ssz 10304 . . . . . . . . . . . . . . . . . . . . . 22
138 mapss 7058 . . . . . . . . . . . . . . . . . . . . . 22
1393, 137, 138mp2an 655 . . . . . . . . . . . . . . . . . . . . 21
140139sseli 3346 . . . . . . . . . . . . . . . . . . . 20
141 elmapssres 26773 . . . . . . . . . . . . . . . . . . . 20
142140, 97, 141sylancl 645 . . . . . . . . . . . . . . . . . . 19
143142adantl 454 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
144136, 143ffvelrnd 5873 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
145144zred 10377 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
146 simplrr 739 . . . . . . . . . . . . . . . . . . 19 mzPoly mzPoly mzPoly
147 mzpf 26795 . . . . . . . . . . . . . . . . . . 19 mzPoly
148146, 147syl 16 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
149 elmapssres 26773 . . . . . . . . . . . . . . . . . . . 20
150140, 101, 149sylancl 645 . . . . . . . . . . . . . . . . . . 19
151150adantl 454 . . . . . . . . . . . . . . . . . 18 mzPoly mzPoly
152148, 151ffvelrnd 5873 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
153152zred 10377 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
154 sumsqeq0 11462 . . . . . . . . . . . . . . . 16
155145, 153, 154syl2anc 644 . . . . . . . . . . . . . . 15 mzPoly mzPoly
156140adantl 454 . . . . . . . . . . . . . . . . 17 mzPoly mzPoly
157 reseq1 5142 . . . . . . . . . . . . . . . . . . . . 21
158157fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20
159158oveq1d 6098 . . . . . . . . . . . . . . . . . . 19
160 reseq1 5142 . . . . . . . . . . . . . . . . . . . . 21
161160fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20
162161oveq1d 6098 . . . . . . . . . . . . . . . . . . 19
163159, 162oveq12d 6101 . . . . . . . . . . . . . . . . . 18
164 eqid 2438 . . . . . . . . . . . . . . . . . 18
165 ovex 6108 . . . . . . . . . . . . . . . . . 18
166163, 164, 165fvmpt 5808 . . . . . . . . . . . . . . . . 17
167156, 166syl 16 . . . . . . . . . . . . . . . 16 mzPoly mzPoly
168167eqeq1d 2446 . . . . . . . . . . . . . . 15 mzPoly mzPoly
169155, 168bitr4d 249 . . . . . . . . . . . . . 14 mzPoly mzPoly
170169anbi2d 686 . . . . . . . . . . . . 13 mzPoly mzPoly
171170rexbidva 2724 . . . . . . . . . . . 12 mzPoly mzPoly
172133, 171bitrd 246 . . . . . . . . . . 11 mzPoly mzPoly
17331, 172syl5bbr 252 . . . . . . . . . 10 mzPoly mzPoly
174173abbidv 2552 . . . . . . . . 9 mzPoly mzPoly
17530, 174syl5eq 2482 . . . . . . . 8 mzPoly mzPoly
176 simpl 445 . . . . . . . . 9 mzPoly mzPoly
177 fzssuz 11095 . . . . . . . . . . . 12
178 uzssz 10507 . . . . . . . . . . . 12
179177, 178sstri 3359 . . . . . . . . . . 11
1803, 179pm3.2i 443 . . . . . . . . . 10
181180a1i 11 . . . . . . . . 9 mzPoly mzPoly
1823a1i 11 . . . . . . . . . . . 12 mzPoly mzPoly
18397a1i 11 . . . . . . . . . . . 12 mzPoly mzPoly
184 simprl 734 . . . . . . . . . . . 12 mzPoly mzPoly mzPoly
185 mzpresrename 26809 . . . . . . . . . . . 12 mzPoly mzPoly
186182, 183, 184, 185syl3anc 1185 . . . . . . . . . . 11 mzPoly mzPoly mzPoly
187 2nn0 10240 . . . . . . . . . . 11
188 mzpexpmpt 26804 . . . . . . . . . . 11 mzPoly mzPoly
189186, 187, 188sylancl 645 . . . . . . . . . 10 mzPoly mzPoly mzPoly
190101a1i 11 . . . . . . . . . . . 12 mzPoly mzPoly
191 simprr 735 . . . . . . . . . . . 12 mzPoly mzPoly mzPoly
192 mzpresrename 26809 . . . . . . . . . . . 12 mzPoly mzPoly
193182, 190, 191, 192syl3anc 1185 . . . . . . . . . . 11 mzPoly mzPoly mzPoly
194 mzpexpmpt 26804 . . . . . . . . . . 11 mzPoly mzPoly
195193, 187, 194sylancl 645 . . . . . . . . . 10 mzPoly mzPoly mzPoly
196 mzpaddmpt 26800 . . . . . . . . . 10 mzPoly mzPoly mzPoly
197189, 195, 196syl2anc 644 . . . . . . . . 9 mzPoly mzPoly mzPoly
198 eldioph2 26822 . . . . . . . . 9 mzPoly Dioph
199176, 181, 197, 198syl3anc 1185 . . . . . . . 8 mzPoly mzPoly Dioph
200175, 199eqeltrd 2512 . . . . . . 7 mzPoly mzPoly Dioph
201 ineq12 3539 . . . . . . . 8
202201eleq1d 2504 . . . . . . 7 Dioph Dioph
203200, 202syl5ibrcom 215 . . . . . 6 mzPoly mzPoly Dioph
204203rexlimdvva 2839 . . . . 5 mzPoly mzPoly Dioph
20529, 204syl5bir 211 . . . 4 mzPoly