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

Theorem 0xr 8894
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 8892 . 2  |-  RR  C_  RR*
2 0re 8854 . 2  |-  0  e.  RR
31, 2sselii 3190 1  |-  0  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   RRcr 8752   0cc0 8753   RR*cxr 8882
This theorem is referenced by:  ge0gtmnf  10517  max0sub  10539  xlt0neg1  10562  xlt0neg2  10563  xle0neg1  10564  xle0neg2  10565  xaddf  10567  xaddid1  10582  xaddid2  10583  xaddge0  10594  xsubge0  10597  xposdif  10598  xmullem  10600  xmullem2  10601  xmul01  10603  xmul02  10604  xmulneg1  10605  xmulf  10608  xmulpnf1  10610  xmulasslem2  10618  xmulge0  10620  xmulasslem  10621  xlemul1a  10624  xadddi  10631  xadddi2  10633  ioopos  10742  ioorebas  10761  elxrge0  10763  xov1plusxeqvd  10796  rpsup  10986  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos1bnd  12483  sinltx  12485  sin01gt0  12486  cos01gt0  12487  sin02gt0  12488  sincos1sgn  12489  sincos2sgn  12490  pcge0  12930  xrge0subm  16428  leordtval2  16958  pnfnei  16966  mnfnei  16967  isxmet2d  17908  xmetge0  17925  xmetgt0  17938  prdsdsf  17947  prdsxmetlem  17948  xpsdsval  17961  blgt0  17972  xblss2  17974  xbln0  17981  prdsbl  18053  stdbdxmet  18077  stdbdmopn  18080  nmoge0  18246  nmo0  18260  cnblcld  18300  blssioo  18317  blcvx  18320  xrsxmet  18331  metdsf  18368  metds0  18370  metdseq0  18374  metnrmlem1a  18378  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  pcoass  18538  iscfil2  18708  ovolmge0  18852  ovolge0  18856  ovolf  18857  ovolssnul  18862  ovolctb  18865  ovoliunnul  18882  ovolicopnf  18899  voliunlem3  18925  volsup  18929  ioorf  18944  volivth  18978  vitalilem4  18982  vitalilem5  18983  itg2ge0  19106  itg2const2  19112  itg2seq  19113  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2gt0  19131  itg2cnlem2  19133  itg2cn  19134  iblss  19175  itgle  19180  itgeqa  19184  ibladdlem  19190  iblabs  19199  iblabsr  19200  iblmulc2  19201  bddmulibl  19209  dvne0  19374  mdegle0  19479  ply1remlem  19564  ply1rem  19565  plypf1  19610  aaliou3lem2  19739  aaliou3lem3  19740  taylfvallem1  19752  taylfval  19754  tayl0  19757  radcnvcl  19809  radcnvle  19812  pserulm  19814  psercnlem1  19817  pilem2  19844  sinhalfpilem  19850  sincosq1lem  19881  sincosq1sgn  19882  sincosq2sgn  19883  tangtx  19889  tanabsge  19890  sinq12gt0  19891  cosq14gt0  19894  sincos4thpi  19897  pige3  19901  cosordlem  19909  tanord1  19915  tanord  19916  efifo  19925  argimgt0  19982  argimlt0  19983  logccv  20026  loglesqr  20114  atantan  20235  rlimcnp  20276  rlimcnp2  20277  rlimcnp3  20278  scvxcvx  20296  basellem1  20334  dchrisum0lem2a  20682  pntibndlem1  20754  pntibnd  20758  pntlemc  20760  pntlem3  20774  abvcxp  20780  padicabvf  20796  padicabvcxp  20797  ostth2  20802  nmooge0  21361  nmoo0  21385  nmlnogt0  21391  nmopge0  22507  nmopgt0  22508  nmfnge0  22523  nmop0  22582  nmfn0  22583  elxrge02  23132  xraddge02  23267  xlt2addrd  23268  unitssxrge0  23299  xrs0  23320  xrge00  23326  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhom  23334  xrge0mulc1cn  23338  xrge0addass  23344  xrge0neqmnf  23345  xrge0addgt0  23346  xrge0adddir  23347  fsumrp0cl  23349  pnfneige0  23389  lmxrge0  23390  hashgt0  23402  esumnul  23442  esum0  23443  esumle  23448  esumlef  23450  esumcst  23451  esumsn  23452  esumpr2  23454  esumpinfval  23456  esumpfinvallem  23457  esumpinfsum  23460  esumpcvgval  23461  esumpmono  23462  esummulc1  23464  hashf2  23467  esumcvg  23469  prob01  23631  probmeasb  23648  dstfrvclim1  23693  cvmliftlem10  23840  cvmliftlem13  23842  sinccvglem  24020  ovoliunnfl  25001  itg2addnclem  25003  itg2addnclem2  25004  itg2gt0cn  25006  ibladdnclem  25007  itgaddnclem2  25010  iblabsnc  25015  iblmulc2nc  25016  bddiblnc  25021  dvreasin  25026  areacirc  25034  iintlem1  25713  rrnequiv  26662  idomrootle  27614  itgsin0pilem1  27847  stoweidlem46  27898  sgn0  28500  sgnp  28501  sgnn  28505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-xr 8887
  Copyright terms: Public domain W3C validator