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

Theorem 0xr 8878
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 8876 . 2  |-  RR  C_  RR*
2 0re 8838 . 2  |-  0  e.  RR
31, 2sselii 3177 1  |-  0  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   RRcr 8736   0cc0 8737   RR*cxr 8866
This theorem is referenced by:  ge0gtmnf  10501  max0sub  10523  xlt0neg1  10546  xlt0neg2  10547  xle0neg1  10548  xle0neg2  10549  xaddf  10551  xaddid1  10566  xaddid2  10567  xaddge0  10578  xsubge0  10581  xposdif  10582  xmullem  10584  xmullem2  10585  xmul01  10587  xmul02  10588  xmulneg1  10589  xmulf  10592  xmulpnf1  10594  xmulasslem2  10602  xmulge0  10604  xmulasslem  10605  xlemul1a  10608  xadddi  10615  xadddi2  10617  ioopos  10726  ioorebas  10745  elxrge0  10747  xov1plusxeqvd  10780  rpsup  10970  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos1bnd  12467  sinltx  12469  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  sincos1sgn  12473  sincos2sgn  12474  pcge0  12914  xrge0subm  16412  leordtval2  16942  pnfnei  16950  mnfnei  16951  isxmet2d  17892  xmetge0  17909  xmetgt0  17922  prdsdsf  17931  prdsxmetlem  17932  xpsdsval  17945  blgt0  17956  xblss2  17958  xbln0  17965  prdsbl  18037  stdbdxmet  18061  stdbdmopn  18064  nmoge0  18230  nmo0  18244  cnblcld  18284  blssioo  18301  blcvx  18304  xrsxmet  18315  metdsf  18352  metds0  18354  metdseq0  18358  metnrmlem1a  18362  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  pcoass  18522  iscfil2  18692  ovolmge0  18836  ovolge0  18840  ovolf  18841  ovolssnul  18846  ovolctb  18849  ovoliunnul  18866  ovolicopnf  18883  voliunlem3  18909  volsup  18913  ioorf  18928  volivth  18962  vitalilem4  18966  vitalilem5  18967  itg2ge0  19090  itg2const2  19096  itg2seq  19097  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2gt0  19115  itg2cnlem2  19117  itg2cn  19118  iblss  19159  itgle  19164  itgeqa  19168  ibladdlem  19174  iblabs  19183  iblabsr  19184  iblmulc2  19185  bddmulibl  19193  dvne0  19358  mdegle0  19463  ply1remlem  19548  ply1rem  19549  plypf1  19594  aaliou3lem2  19723  aaliou3lem3  19724  taylfvallem1  19736  taylfval  19738  tayl0  19741  radcnvcl  19793  radcnvle  19796  pserulm  19798  psercnlem1  19801  pilem2  19828  sinhalfpilem  19834  sincosq1lem  19865  sincosq1sgn  19866  sincosq2sgn  19867  tangtx  19873  tanabsge  19874  sinq12gt0  19875  cosq14gt0  19878  sincos4thpi  19881  pige3  19885  cosordlem  19893  tanord1  19899  tanord  19900  efifo  19909  argimgt0  19966  argimlt0  19967  logccv  20010  loglesqr  20098  atantan  20219  rlimcnp  20260  rlimcnp2  20261  rlimcnp3  20262  scvxcvx  20280  basellem1  20318  dchrisum0lem2a  20666  pntibndlem1  20738  pntibnd  20742  pntlemc  20744  pntlem3  20758  abvcxp  20764  padicabvf  20780  padicabvcxp  20781  ostth2  20786  nmooge0  21345  nmoo0  21369  nmlnogt0  21375  nmopge0  22491  nmopgt0  22492  nmfnge0  22507  nmop0  22566  nmfn0  22567  elxrge02  23116  xraddge02  23252  xlt2addrd  23253  unitssxrge0  23284  xrs0  23305  xrge00  23311  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhom  23319  xrge0mulc1cn  23323  xrge0addass  23329  xrge0neqmnf  23330  xrge0addgt0  23331  xrge0adddir  23332  fsumrp0cl  23334  pnfneige0  23374  lmxrge0  23375  hashgt0  23387  esumnul  23427  esum0  23428  esumle  23433  esumlef  23435  esumcst  23436  esumsn  23437  esumpr2  23439  esumpinfval  23441  esumpfinvallem  23442  esumpinfsum  23445  esumpcvgval  23446  esumpmono  23447  esummulc1  23449  hashf2  23452  esumcvg  23454  prob01  23616  probmeasb  23633  dstfrvclim1  23678  cvmliftlem10  23825  cvmliftlem13  23827  sinccvglem  24005  dvreasin  24923  areacirc  24931  iintlem1  25610  rrnequiv  26559  idomrootle  27511  itgsin0pilem1  27744  stoweidlem46  27795  sgn0  28246  sgnp  28247  sgnn  28251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-xr 8871
  Copyright terms: Public domain W3C validator