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

Theorem rmxdioph 27422
Description: X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.)
Assertion
Ref Expression
rmxdioph

Proof of Theorem rmxdioph
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 449 . . . . . 6
2 elmapi 7091 . . . . . . . 8
3 df-3 10114 . . . . . . . . . 10
4 ssid 3360 . . . . . . . . . 10
53, 4jm2.27dlem5 27419 . . . . . . . . 9
6 2nn 10188 . . . . . . . . . 10
76jm2.27dlem3 27417 . . . . . . . . 9
85, 7sselii 3338 . . . . . . . 8
9 ffvelrn 5920 . . . . . . . 8
102, 8, 9sylancl 645 . . . . . . 7
1110adantr 453 . . . . . 6
12 3nn 10189 . . . . . . . . 9
1312jm2.27dlem3 27417 . . . . . . . 8
14 ffvelrn 5920 . . . . . . . 8
152, 13, 14sylancl 645 . . . . . . 7
1615adantr 453 . . . . . 6
17 rmxdiophlem 27421 . . . . . 6
181, 11, 16, 17syl3anc 1185 . . . . 5
1918pm5.32da 624 . . . 4
20 anass 632 . . . . . 6
2120rexbii 2741 . . . . 5
22 r19.42v 2873 . . . . 5
2321, 22bitr2i 243 . . . 4
2419, 23syl6bb 254 . . 3
2524rabbiia 2959 . 2
26 3nn0 10294 . . 3
27 vex 2972 . . . . . . . 8
2827resex 5234 . . . . . . 7
29 fvex 5789 . . . . . . 7
30 df-2 10113 . . . . . . . . . . . . . 14
3130, 5jm2.27dlem5 27419 . . . . . . . . . . . . 13
32 1nn 10066 . . . . . . . . . . . . . 14
3332jm2.27dlem3 27417 . . . . . . . . . . . . 13
3431, 33sselii 3338 . . . . . . . . . . . 12
3534jm2.27dlem1 27415 . . . . . . . . . . 11
3635eleq1d 2513 . . . . . . . . . 10
3736adantr 453 . . . . . . . . 9
38 simpr 449 . . . . . . . . . 10
398jm2.27dlem1 27415 . . . . . . . . . . . 12
4035, 39oveq12d 6151 . . . . . . . . . . 11
4140adantr 453 . . . . . . . . . 10
4238, 41eqeq12d 2461 . . . . . . . . 9
4337, 42anbi12d 693 . . . . . . . 8
4413jm2.27dlem1 27415 . . . . . . . . . . . 12
4544oveq1d 6148 . . . . . . . . . . 11
4645adantr 453 . . . . . . . . . 10
4735oveq1d 6148 . . . . . . . . . . . 12
4847oveq1d 6148 . . . . . . . . . . 11
49 oveq1 6140 . . . . . . . . . . 11
5048, 49oveqan12d 6152 . . . . . . . . . 10
5146, 50oveq12d 6151 . . . . . . . . 9
5251eqeq1d 2455 . . . . . . . 8
5343, 52anbi12d 693 . . . . . . 7
5428, 29, 53sbc2ie 3248 . . . . . 6
5554a1i 11 . . . . 5
5655rabbiia 2959 . . . 4
57 4nn0 10295 . . . . . 6
58 rmydioph 27420 . . . . . 6
59 simp1 958 . . . . . . . . 9
6059eleq1d 2513 . . . . . . . 8
61 simp3 960 . . . . . . . . 9
62 simp2 959 . . . . . . . . . 10
6359, 62oveq12d 6151 . . . . . . . . 9
6461, 63eqeq12d 2461 . . . . . . . 8
6560, 64anbi12d 693 . . . . . . 7
66 df-4 10115 . . . . . . . . . . 11
67 ssid 3360 . . . . . . . . . . 11
6866, 67jm2.27dlem5 27419 . . . . . . . . . 10
693, 68jm2.27dlem5 27419 . . . . . . . . 9
7030, 69jm2.27dlem5 27419 . . . . . . . 8
7170, 33sselii 3338 . . . . . . 7
7269, 7sselii 3338 . . . . . . 7
73 4nn 10190 . . . . . . . 8
7473jm2.27dlem3 27417 . . . . . . 7
7565, 71, 72, 74rabren3dioph 27211 . . . . . 6
7657, 58, 75mp2an 655 . . . . 5
77 ovex 6158 . . . . . . . . 9
7868, 13sselii 3338 . . . . . . . . 9
79 mzpproj 27131 . . . . . . . . 9
8077, 78, 79mp2an 655 . . . . . . . 8
81 2nn0 10293 . . . . . . . 8
82 mzpexpmpt 27139 . . . . . . . 8
8380, 81, 82mp2an 655 . . . . . . 7
84 mzpproj 27131 . . . . . . . . . . 11
8577, 71, 84mp2an 655 . . . . . . . . . 10
86 mzpexpmpt 27139 . . . . . . . . . 10
8785, 81, 86mp2an 655 . . . . . . . . 9
88 1z 10366 . . . . . . . . . 10
89 mzpconstmpt 27134 . . . . . . . . . 10
9077, 88, 89mp2an 655 . . . . . . . . 9
91 mzpsubmpt 27137 . . . . . . . . 9
9287, 90, 91mp2an 655 . . . . . . . 8
93 mzpproj 27131 . . . . . . . . . 10
9477, 74, 93mp2an 655 . . . . . . . . 9
95 mzpexpmpt 27139 . . . . . . . . 9
9694, 81, 95mp2an 655 . . . . . . . 8
97 mzpmulmpt 27136 . . . . . . . 8
9892, 96, 97mp2an 655 . . . . . . 7
99 mzpsubmpt 27137 . . . . . . 7
10083, 98, 99mp2an 655 . . . . . 6
101 eqrabdioph 27173 . . . . . 6
10257, 100, 90, 101mp3an 1280 . . . . 5
103 anrabdioph 27176 . . . . 5
10476, 102, 103mp2an 655 . . . 4
10556, 104eqeltri 2517 . . 3
10666rexfrabdioph 27190 . . 3
10726, 105, 106mp2an 655 . 2
10825, 107eqeltri 2517 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  /\wa 360  /\w3a 937  =wceq 1654  e.wcel 1728  E.wrex 2717  {crab 2720   cvv 2969  [.wsbc 3174  e.cmpt 4305  |`cres 4925  -->wf 5501  `cfv 5505  (class class class)co 6133   cmap 7071  1c1 9046   cmul 9050   cmin 9346  2c2 10104  3c3 10105  4c4 10106   cn0 10276   cz 10337   cuz 10543   cfz 11098   cexp 11437   cmzp 27116   cdioph 27150   crmx 27298   crmy 27299
This theorem is referenced by:  expdiophlem2  27428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-rep 4358  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446  ax-un 4746  ax-inf2 7649  ax-cnex 9101  ax-resscn 9102  ax-1cn 9103  ax-icn 9104  ax-addcl 9105  ax-addrcl 9106  ax-mulcl 9107  ax-mulrcl 9108  ax-mulcom 9109  ax-addass 9110  ax-mulass 9111  ax-distr 9112  ax-i2m1 9113  ax-1ne0 9114  ax-1rid 9115  ax-rnegex 9116  ax-rrecex 9117  ax-cnre 9118  ax-pre-lttri 9119  ax-pre-lttrn 9120  ax-pre-ltadd 9121  ax-pre-mulgt0 9122  ax-pre-sup 9123  ax-addf 9124  ax-mulf 9125
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-nel 2613  df-ral 2721  df-rex 2722  df-reu 2723  df-rmo 2724  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3621  df-if 3770  df-pw 3832  df-sn 3851  df-pr 3852  df-tp 3853  df-op 3854  df-uni 4048  df-int 4084  df-iun 4128  df-iin 4129  df-br 4248  df-opab 4306  df-mpt 4307  df-tr 4341  df-eprel 4539  df-id 4543  df-po 4548  df-so 4549  df-fr 4586  df-se 4587  df-we 4588  df-ord 4629  df-on 4630  df-lim 4631  df-suc 4632  df-om 4891  df-xp 4929  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512  df-fv 5513  df-isom 5514  df-ov 6136  df-oprab 6137  df-mpt2 6138  df-of 6359  df-1st 6403  df-2nd 6404  df-riota 6603  df-recs 6686  df-rdg 6721  df-1o 6777  df-2o 6778  df-oadd 6781  df-omul 6782  df-er 6958  df-map 7073  df-pm 7074  df-ixp 7117  df-en 7163  df-dom 7164  df-sdom 7165  df-fin 7166  df-fi 7469  df-sup 7499  df-oi 7532  df-card 7881  df-acn 7884  df-cda 8103  df-pnf 9177  df-mnf 9178  df-xr 9179  df-ltxr 9180  df-le 9181  df-sub 9348  df-neg 9349  df-div 9733  df-nn 10056  df-2 10113  df-3 10114  df-4 10115  df-5 10116  df-6 10117  df-7 10118  df-8 10119  df-9 10120  df-10 10121  df-n0 10277  df-z 10338  df-dec 10438  df-uz 10544  df-q 10630  df-rp 10668  df-xneg 10765  df-xadd 10766  df-xmul 10767  df-ioo 10975  df-ioc 10976  df-ico 10977  df-icc 10978  df-fz 11099  df-fzo 11191  df-fl 11257  df-mod 11306  df-seq 11379  df-exp 11438  df-fac 11622  df-bc 11649  df-hash 11674  df-shft 11937  df-cj 11959  df-re 11960  df-im 11961  df-sqr 12095  df-abs 12096  df-limsup 12320  df-clim 12337  df-rlim 12338  df-sum 12535  df-ef 12725  df-sin 12727  df-cos 12728  df-pi 12730  df-dvds 12908  df-gcd 13062  df-prm 13135  df-numer 13182  df-denom 13183  df-struct 13526  df-ndx 13527  df-slot 13528  df-base 13529  df-sets 13530  df-ress 13531  df-plusg 13597  df-mulr 13598  df-starv 13599  df-sca 13600  df-vsca 13601  df-tset 13603  df-ple 13604  df-ds 13606  df-unif 13607  df-hom 13608  df-cco 13609  df-rest 13705  df-topn 13706  df-topgen 13722  df-pt 13723  df-prds 13726  df-xrs 13781  df-0g 13782  df-gsum 13783  df-qtop 13788  df-imas 13789  df-xps 13791  df-mre 13866  df-mrc 13867  df-acs 13869  df-mnd 14726  df-submnd 14775  df-mulg 14851  df-cntz 15152  df-cmn 15450  df-psmet 16730  df-xmet 16731  df-met 16732  df-bl 16733  df-mopn 16734  df-fbas 16735  df-fg 16736  df-cnfld 16740  df-top 16999  df-bases 17001  df-topon 17002  df-topsp 17003  df-cld 17119  df-ntr 17120  df-cls 17121  df-nei 17198  df-lp 17236  df-perf 17237  df-cn 17327  df-cnp 17328  df-haus 17415  df-tx 17630  df-hmeo 17823  df-fil 17914  df-fm 18006  df-flim 18007  df-flf 18008  df-xms 18386  df-ms 18387  df-tms 18388  df-cncf 18944  df-limc 19789  df-dv 19790  df-log 20490  df-mzpcl 27117  df-mzp 27118  df-dioph 27151  df-squarenn 27239  df-pell1qr 27240  df-pell14qr 27241  df-pell1234qr 27242  df-pellfund 27243  df-rmx 27300  df-rmy 27301
  Copyright terms: Public domain W3C validator