Theorem 0xr 9689

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	|- 0 e. RR*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 9686	. 2 |- RR C_ RR*
2		0re 9645	. 2 |- 0 e. RR
3	1, 2	sselii 3462	1 |- 0 e. RR*

Syntax hints:   e. wcel 1869   RRcr 9540   0cc0 9541   RR*cxr 9676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-i2m1 9609  ax-1ne0 9610  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306  df-xr 9681

This theorem is referenced by:  0lepnf  11435  ge0gtmnf  11469  max0sub  11491  xlt0neg1  11514  xlt0neg2  11515  xle0neg1  11516  xle0neg2  11517  xaddf  11519  xaddid1  11534  xaddid2  11535  xaddge0  11546  xsubge0  11549  xposdif  11550  xmullem  11552  xmullem2  11553  xmul01  11555  xmul02  11556  xmulneg1  11557  xmulf  11560  xmulpnf1  11562  xmulasslem2  11570  xmulge0  11572  xmulasslem  11573  xlemul1a  11576  xadddi  11583  xadddi2  11585  ioopos  11713  ioorebas  11738  xrge0neqmnf  11739  elxrge0  11743  0e0iccpnf  11745  xov1plusxeqvd  11780  ico01fl0  12054  rpsup  12094  addmodid  12140  hashgt0  12568  hashle00  12578  hashgt0elex  12579  sgn0  13146  sgnp  13147  sgnn  13151  fprodge0  14040  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  cos1bnd  14234  sinltx  14236  sin01gt0  14237  cos01gt0  14238  sin02gt0  14239  sincos1sgn  14240  sincos2sgn  14241  xrsmgm  18996  leordtval2  20220  pnfnei  20228  mnfnei  20229  psmetge0  21320  isxmet2d  21334  xmetge0  21351  xmetgt0  21365  prdsdsf  21374  prdsxmetlem  21375  xpsdsval  21388  blgt0  21406  xblss2ps  21408  xblss2  21409  xbln0  21421  prdsbl  21498  stdbdxmet  21522  stdbdmopn  21525  metustto  21560  metustid  21561  metustexhalf  21563  cfilucfil  21566  blval2  21569  metuel2  21572  nmoge0  21718  nmoge0OLD  21736  nmo0  21748  cnblcld  21787  blssioo  21805  blcvx  21808  xrsxmet  21819  metdsf  21857  metds0  21859  metdseq0  21863  metnrmlem1a  21867  metdsfOLD  21872  metds0OLD  21874  metdseq0OLD  21878  metnrmlem1aOLD  21882  iccpnfcnv  21964  iccpnfhmeo  21965  xrhmeo  21966  pcoass  22047  iscfil2  22228  ovolmge0  22422  ovolge0  22426  ovolf  22427  ovolssnul  22432  ovolctb  22435  ovoliunnul  22452  ovolicopnf  22470  voliunlem3  22497  volsup  22501  ioorf  22517  ioorfOLD  22522  volivth  22557  vitalilem4  22561  vitalilem5  22562  itg2ge0  22685  itg2const2  22691  itg2seq  22692  itg2monolem1  22700  itg2monolem2  22701  itg2monolem3  22702  itg2gt0  22710  dvne0  22955  mdegle0  23018  ply1remlem  23105  ply1rem  23106  plypf1  23158  aaliou3lem2  23291  aaliou3lem3  23292  taylfvallem1  23304  taylfval  23306  tayl0  23309  radcnvcl  23364  radcnvle  23367  pserulm  23369  psercnlem1  23372  pilem2  23399  pilem2OLD  23400  sinhalfpilem  23410  sincosq1lem  23444  sincosq1sgn  23445  sincosq2sgn  23446  tangtx  23452  tanabsge  23453  sinq12gt0  23454  cosq14gt0  23457  sincos4thpi  23460  pige3  23464  cosordlem  23472  tanord1  23478  tanord  23479  efifo  23488  argimgt0  23553  argimlt0  23554  logccv  23600  loglesqrt  23690  atantan  23841  rlimcnp  23883  rlimcnp2  23884  scvxcvx  23903  basellem1  23999  dchrisum0lem2a  24347  pntibndlem1  24419  pntibnd  24423  pntlemc  24425  pntlem3  24439  abvcxp  24445  padicabvf  24461  padicabvcxp  24462  ostth2  24467  ttgcontlem1  24907  nmooge0  26400  nmoo0  26424  nmlnogt0  26430  nmopge0  27556  nmopgt0  27557  nmfnge0  27572  nmop0  27631  nmfn0  27632  xraddge02  28336  xlt2addrd  28338  xrge0infss  28340  xrge0infssOLD  28341  dfrp2  28352  elxrge02  28402  xrs0  28438  xrge00  28449  xrge0addass  28453  xrge0addgt0  28455  xrge0adddir  28456  fsumrp0cl  28459  metider  28699  unitssxrge0  28708  xrge0iifcnv  28741  xrge0iifcv  28742  xrge0iifiso  28743  xrge0iifhom  28745  xrge0mulc1cn  28749  pnfneige0  28759  lmxrge0  28760  esumgsum  28868  esumnul  28871  esum0  28872  esumle  28881  esumlef  28885  esumcst  28886  esumsnf  28887  esumpr2  28890  esumpinfval  28896  esumpinfsum  28900  esumpcvgval  28901  esumpmono  28902  hashf2  28907  esumcvg  28909  measle0  29032  voliune  29054  volfiniune  29055  ddemeas  29061  aean  29069  oms0  29127  oms0OLD  29131  prob01  29248  probmeasb  29265  dstfrvclim1  29312  sgncl  29411  sgn3da  29414  signsply0  29442  cvmliftlem10  30019  cvmliftlem13  30021  sinccvglem  30318  sin2h  31893  tan2h  31895  broucube  31932  mblfinlem2  31936  ovoliunnfl  31940  voliunnfl  31942  volsupnfl  31943  mbfposadd  31946  itg2addnclem2  31952  itg2gt0cn  31955  ftc1anclem5  31979  ftc1anclem8  31982  dvasin  31986  areacirc  31995  rrnequiv  32125  idomrootle  36033  imo72b2  36521  xadd0ge  37428  xrge0nemnfd  37441  pnfel0pnf  37504  ge0nemnf2  37505  ge0xrre  37508  fsumge0cl  37519  sinaover2ne0  37607  itgsin0pilem1  37690  iblsplit  37707  stoweidlem46  37771  fourierdlem43  37878  fourierdlem44  37879  fourierdlem60  37894  fourierdlem61  37895  fourierdlem87  37921  fourierdlem103  37937  fourierdlem104  37938  fourierdlem111  37945  sqwvfourb  37957  fourierswlem  37958  fouriersw  37959  etransclem23  37986  fge0npnf  38041  fge0iccico  38044  gsumge0cl  38045  sge0z  38049  sge00  38050  sge0sn  38053  sge0tsms  38054  sge0cl  38055  sge0f1o  38056  sge0ge0  38058  sge0repnf  38060  sge0fsum  38061  sge0pr  38068  sge0ssre  38071  sge0prle  38075  sge0p1  38088  sge0iunmptlemre  38089  sge0rpcpnf  38095  sge0rernmpt  38096  sge0isum  38101  sge0ad2en  38105  sge0xaddlem2  38108  omessre  38154  omeiunltfirp  38163  carageniuncllem2  38166  carageniuncl  38167  hoiprodcl  38188  ovnlerp  38203  ovnf  38204  ovn0lem  38206  ovnsubaddlem1  38211