MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0xr Structured version   Unicode version

Theorem 0xr 9136
Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
Assertion
Ref Expression
0xr  |-  0  e.  RR*

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 9134 . 2  |-  RR  C_  RR*
2 0re 9096 . 2  |-  0  e.  RR
31, 2sselii 3347 1  |-  0  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   RRcr 8994   0cc0 8995   RR*cxr 9124
This theorem is referenced by:  nn0pnfge0  10733  ge0gtmnf  10765  max0sub  10787  xlt0neg1  10810  xlt0neg2  10811  xle0neg1  10812  xle0neg2  10813  xaddf  10815  xaddid1  10830  xaddid2  10831  xaddge0  10842  xsubge0  10845  xposdif  10846  xmullem  10848  xmullem2  10849  xmul01  10851  xmul02  10852  xmulneg1  10853  xmulf  10856  xmulpnf1  10858  xmulasslem2  10866  xmulge0  10868  xmulasslem  10869  xlemul1a  10872  xadddi  10879  xadddi2  10881  ioopos  10992  ioorebas  11011  elxrge0  11013  xov1plusxeqvd  11046  rpsup  11252  hashgt0  11667  hashle00  11674  hashgt0elex  11675  ef01bndlem  12790  sin01bnd  12791  cos01bnd  12792  cos1bnd  12793  sinltx  12795  sin01gt0  12796  cos01gt0  12797  sin02gt0  12798  sincos1sgn  12799  sincos2sgn  12800  pcge0  13240  xrge0subm  16744  leordtval2  17281  pnfnei  17289  mnfnei  17290  psmetge0  18348  isxmet2d  18362  xmetge0  18379  xmetgt0  18393  prdsdsf  18402  prdsxmetlem  18403  xpsdsval  18416  blgt0  18434  xblss2ps  18436  xblss2  18437  xbln0  18449  prdsbl  18526  stdbdxmet  18550  stdbdmopn  18553  metusttoOLD  18592  metustto  18593  metustidOLD  18594  metustid  18595  metustexhalfOLD  18598  metustexhalf  18599  cfilucfilOLD  18604  cfilucfil  18605  blval2  18610  metuel2  18614  nmoge0  18760  nmo0  18774  cnblcld  18814  blssioo  18831  blcvx  18834  xrsxmet  18845  metdsf  18883  metds0  18885  metdseq0  18889  metnrmlem1a  18893  iccpnfcnv  18974  iccpnfhmeo  18975  xrhmeo  18976  pcoass  19054  iscfil2  19224  ovolmge0  19378  ovolge0  19382  ovolf  19383  ovolssnul  19388  ovolctb  19391  ovoliunnul  19408  ovolicopnf  19425  voliunlem3  19451  volsup  19455  ioorf  19470  volivth  19504  vitalilem4  19508  vitalilem5  19509  itg2ge0  19630  itg2const2  19636  itg2seq  19637  itg2splitlem  19643  itg2split  19644  itg2monolem1  19645  itg2monolem2  19646  itg2monolem3  19647  itg2gt0  19655  itg2cnlem2  19657  itg2cn  19658  iblss  19699  itgle  19704  itgeqa  19708  ibladdlem  19714  iblabs  19723  iblabsr  19724  iblmulc2  19725  bddmulibl  19733  dvne0  19900  mdegle0  20005  ply1remlem  20090  ply1rem  20091  plypf1  20136  aaliou3lem2  20265  aaliou3lem3  20266  taylfvallem1  20278  taylfval  20280  tayl0  20283  radcnvcl  20338  radcnvle  20341  pserulm  20343  psercnlem1  20346  pilem2  20373  sinhalfpilem  20379  sincosq1lem  20410  sincosq1sgn  20411  sincosq2sgn  20412  tangtx  20418  tanabsge  20419  sinq12gt0  20420  cosq14gt0  20423  sincos4thpi  20426  pige3  20430  cosordlem  20438  tanord1  20444  tanord  20445  efifo  20454  argimgt0  20512  argimlt0  20513  logccv  20559  loglesqr  20647  atantan  20768  rlimcnp  20809  rlimcnp2  20810  rlimcnp3  20811  scvxcvx  20829  basellem1  20868  dchrisum0lem2a  21216  pntibndlem1  21288  pntibnd  21292  pntlemc  21294  pntlem3  21308  abvcxp  21314  padicabvf  21330  padicabvcxp  21331  ostth2  21336  nmooge0  22273  nmoo0  22297  nmlnogt0  22303  nmopge0  23419  nmopgt0  23420  nmfnge0  23435  nmop0  23494  nmfn0  23495  xraddge02  24128  xlt2addrd  24129  elxrge02  24183  xrs0  24202  xrge00  24213  xrge0addass  24216  xrge0neqmnf  24217  xrge0addgt0  24219  xrge0adddir  24220  fsumrp0cl  24222  metider  24294  unitssxrge0  24303  xrge0iifcnv  24324  xrge0iifcv  24325  xrge0iifiso  24326  xrge0iifhom  24328  xrge0mulc1cn  24332  pnfneige0  24341  lmxrge0  24342  esumnul  24448  esum0  24449  esumle  24454  esumlef  24459  esumcst  24460  esumsn  24461  esumpr2  24463  esumpinfval  24468  esumpfinvallem  24469  esumpinfsum  24472  esumpcvgval  24473  esumpmono  24474  esummulc1  24476  hashf2  24479  esumcvg  24481  measle0  24567  voliune  24590  volfiniune  24591  aean  24600  prob01  24676  probmeasb  24693  dstfrvclim1  24740  cvmliftlem10  24986  cvmliftlem13  24988  sinccvglem  25114  sin2h  26250  tan2h  26252  mblfinlem2  26256  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  mbfposadd  26266  itg2addnclem2  26271  itg2gt0cn  26274  ibladdnclem  26275  iblabsnc  26283  iblmulc2nc  26284  bddiblnc  26289  ftc1anclem5  26298  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  dvreasin  26304  areacirc  26311  rrnequiv  26558  idomrootle  27502  itgsin0pilem1  27734  stoweidlem46  27785  sgn0  28593  sgnp  28594  sgnn  28598
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 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-i2m1 9063  ax-1ne0 9064  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-xr 9129
  Copyright terms: Public domain W3C validator