Theorem 0xr 11150

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

Assertion

Ref	Expression
0xr	⊢ 0 ∈ ℝ*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 11147	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11105	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3928	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2109  ℝcr 10996  0cc0 10997  ℝ^*cxr 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11055  ax-addrcl 11058  ax-rnegex 11068  ax-cnre 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3435  df-un 3904  df-ss 3916  df-xr 11141

This theorem is referenced by:  0lepnf  13023  ge0gtmnf  13062  max0sub  13086  xlt0neg1  13109  xlt0neg2  13110  xle0neg1  13111  xle0neg2  13112  xaddf  13114  xaddrid  13131  xaddlid  13132  xnn0xadd0  13137  xaddge0  13148  xsubge0  13151  xposdif  13152  xmullem  13154  xmullem2  13155  xmul01  13157  xmul02  13158  xmulneg1  13159  xmulf  13162  xmulpnf1  13164  xmulasslem2  13172  xmulge0  13174  xmulasslem  13175  xlemul1a  13178  xadddi  13185  xadddi2  13187  dfrp2  13285  ioopos  13315  ioorebas  13342  xrge0neqmnf  13343  elxrge0  13348  0e0iccpnf  13350  xov1plusxeqvd  13389  xnn0xrge0  13397  ico01fl0  13711  rpsup  13758  addmodid  13814  hashgt0  14283  hashle00  14295  hashgt0elex  14296  hashgt23el  14319  sgn0  14983  sgnp  14984  sgnn  14988  fprodge0  15887  ef01bndlem  16080  sin01bnd  16081  cos01bnd  16082  cos1bnd  16083  sinltx  16085  sin01gt0  16086  cos01gt0  16087  sin02gt0  16088  sincos1sgn  16089  sincos2sgn  16090  halfleoddlt  16260  xrsmgm  21297  leordtval2  23081  pnfnei  23089  mnfnei  23090  psmetge0  24181  isxmet2d  24196  xmetge0  24213  xmetgt0  24227  prdsdsf  24236  prdsxmetlem  24237  xpsdsval  24250  blgt0  24268  xblss2ps  24270  xblss2  24271  xbln0  24283  prdsbl  24360  stdbdxmet  24384  stdbdmopn  24387  metustto  24422  metustid  24423  metustexhalf  24425  cfilucfil  24428  blval2  24431  metuel2  24434  nmoge0  24590  nmo0  24604  cnblcld  24643  blssioo  24664  blcvx  24667  xrsxmet  24679  metdsf  24718  metds0  24720  metdseq0  24724  metnrmlem1a  24728  iccpnfcnv  24823  iccpnfhmeo  24824  xrhmeo  24825  pcoass  24905  iscfil2  25147  ovolmge0  25359  ovolge0  25363  ovolf  25364  ovolssnul  25369  ovolctb  25372  ovoliunnul  25389  ovolicopnf  25406  voliunlem3  25434  volsup  25438  ioorf  25455  volivth  25489  vitalilem4  25493  vitalilem5  25494  itg2ge0  25617  itg2const2  25623  itg2seq  25624  itg2monolem1  25632  itg2monolem2  25633  itg2monolem3  25634  itg2gt0  25642  dvne0  25897  mdegle0  25963  ply1remlem  26051  ply1rem  26052  idomrootle  26059  plypf1  26098  aaliou3lem2  26232  aaliou3lem3  26233  taylfvallem1  26245  taylfval  26247  tayl0  26250  radcnvcl  26307  radcnvle  26310  pserulm  26312  psercnlem1  26316  pilem2  26343  sinhalfpilem  26353  sincosq1lem  26387  sincosq1sgn  26388  sincosq2sgn  26389  tangtx  26395  tanabsge  26396  sinq12gt0  26397  cosq14gt0  26400  sincos4thpi  26403  pige3ALT  26410  cos02pilt1  26416  cosq34lt1  26417  cosordlem  26420  cos0pilt1  26422  tanord1  26427  tanord  26428  efifo  26437  argimgt0  26502  argimlt0  26503  logccv  26553  loglesqrt  26652  atantan  26814  rlimcnp  26856  rlimcnp2  26857  scvxcvx  26877  basellem1  26972  dchrisum0lem2a  27409  pntibndlem1  27481  pntibnd  27485  pntlemc  27487  pntlem3  27501  abvcxp  27507  padicabvf  27523  padicabvcxp  27524  ostth2  27529  ttgcontlem1  28817  elntg2  28917  nmooge0  30698  nmoo0  30722  nmlnogt0  30728  nmopge0  31842  nmopgt0  31843  nmfnge0  31858  nmop0  31917  nmfn0  31918  xraddge02  32692  xlt2addrd  32694  xrge0infss  32695  sgncl  32769  sgn3da  32772  elxrge02  32867  xrs0  32955  xrge00  32963  xrge0addass  32965  xrge0addgt0  32966  xrge0adddir  32967  fsumrp0cl  32970  ply1unit  33506  rtelextdg2lem  33707  metider  33875  unitssxrge0  33881  xrge0iifcnv  33914  xrge0iifcv  33915  xrge0iifiso  33916  xrge0iifhom  33918  xrge0mulc1cn  33922  pnfneige0  33932  lmxrge0  33933  esumgsum  34026  esumnul  34029  esum0  34030  esumle  34039  esumlef  34043  esumcst  34044  esumsnf  34045  esumpr2  34048  esumpinfval  34054  esumpinfsum  34058  esumpcvgval  34059  esumpmono  34060  hashf2  34065  esumcvg  34067  measle0  34189  voliune  34210  volfiniune  34211  ddemeas  34217  aean  34225  oms0  34278  prob01  34394  probmeasb  34411  dstfrvclim1  34459  signsply0  34532  chtvalz  34610  hgt750lemf  34634  cvmliftlem10  35284  cvmliftlem13  35286  sinccvglem  35662  dnizeq0  36466  iccioo01  37318  sin2h  37607  tan2h  37609  broucube  37651  mblfinlem2  37655  ovoliunnfl  37659  voliunnfl  37661  volsupnfl  37662  mbfposadd  37664  itg2addnclem2  37669  itg2gt0cn  37672  ftc1anclem5  37694  ftc1anclem8  37697  dvasin  37701  areacirc  37710  rrnequiv  37832  dvrelog2b  42056  aks6d1c5lem3  42127  aks6d1c6lem1  42160  acos1half  42348  redvmptabs  42350  readvrec2  42351  readvrec  42352  imo72b2  44162  absfico  45212  xadd0ge  45317  xrge0nemnfd  45328  xralrple2  45350  xrpnf  45480  pnfel0pnf  45525  ge0xrre  45528  sqrlearg  45550  fsumge0cl  45570  limsup10ex  45768  liminf10ex  45769  sinaover2ne0  45863  itgsin0pilem1  45945  iblsplit  45961  stoweidlem46  46041  fourierdlem43  46145  fourierdlem44  46146  fourierdlem60  46161  fourierdlem61  46162  fourierdlem87  46188  fourierdlem103  46204  fourierdlem104  46205  fourierdlem111  46212  sqwvfourb  46224  fourierswlem  46225  fouriersw  46226  etransclem23  46252  salexct2  46334  fge0npnf  46362  fge0iccico  46365  gsumge0cl  46366  sge0z  46370  sge00  46371  sge0sn  46374  sge0tsms  46375  sge0cl  46376  sge0f1o  46377  sge0ge0  46379  sge0repnf  46381  sge0fsum  46382  sge0pr  46389  sge0ssre  46392  sge0prle  46396  sge0p1  46409  sge0iunmptlemre  46410  sge0rpcpnf  46416  sge0rernmpt  46417  sge0isum  46422  sge0ad2en  46426  sge0xaddlem2  46429  sge0uzfsumgt  46439  sge0seq  46441  sge0reuz  46442  voliunsge0lem  46467  meage0  46470  meassre  46472  meale0eq0  46473  meaiuninclem  46475  omessre  46505  omeiunltfirp  46514  carageniuncllem2  46517  carageniuncl  46518  omege0  46528  omess0  46529  hoiprodcl  46542  ovnlerp  46557  ovnf  46558  ovn0lem  46560  ovnsubaddlem1  46565  hoiprodcl3  46575  hoidmvcl  46577  hoidmv1lelem3  46588  hoidmvlelem5  46594  ovnhoilem1  46596  ovolval5lem1  46647  pimrecltneg  46719  rehalfge1  47333  mod42tp1mod8  47600  eenglngeehlnmlem1  48736  eenglngeehlnmlem2  48737  rrxsphere  48747  itscnhlinecirc02p  48784  iooii  48916  io1ii  48919  sepfsepc  48926  seppcld  48928