Theorem 0xr 11215

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 11212	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11169	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3924	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2132  ℝcr 11058  0cc0 11059  ℝ^*cxr 11201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-1cn 11117  ax-addrcl 11120  ax-rnegex 11130  ax-cnre 11132

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rex 3077  df-v 3446  df-un 3900  df-ss 3912  df-xr 11206

This theorem is referenced by:  0lepnf  13121  ge0gtmnf  13161  max0sub  13185  xlt0neg1  13208  xlt0neg2  13209  xle0neg1  13210  xle0neg2  13211  xaddf  13213  xaddrid  13230  xaddlid  13231  xnn0xadd0  13236  xaddge0  13247  xsubge0  13250  xposdif  13251  xmullem  13253  xmullem2  13254  xmul01  13256  xmul02  13257  xmulneg1  13258  xmulf  13261  xmulpnf1  13263  xmulasslem2  13271  xmulge0  13273  xmulasslem  13274  xlemul1a  13277  xadddi  13284  xadddi2  13286  dfrp2  13384  ioopos  13414  ioorebas  13441  xrge0neqmnf  13442  elxrge0  13447  0e0iccpnf  13449  xov1plusxeqvd  13488  xnn0xrge0  13496  ico01fl0  13815  rpsup  13862  addmodid  13918  hashgt0  14387  hashle00  14399  hashgt0elex  14400  hashgt23el  14423  sgn0  15088  sgnp  15089  sgnn  15093  fprodge0  15995  ef01bndlem  16188  sin01bnd  16189  cos01bnd  16190  cos1bnd  16191  sinltx  16193  sin01gt0  16194  cos01gt0  16195  sin02gt0  16196  sincos1sgn  16197  sincos2sgn  16198  halfleoddlt  16368  xrsmgm  21428  leordtval2  23241  pnfnei  23249  mnfnei  23250  psmetge0  24341  isxmet2d  24356  xmetge0  24373  xmetgt0  24387  prdsdsf  24396  prdsxmetlem  24397  xpsdsval  24410  blgt0  24428  xblss2ps  24430  xblss2  24431  xbln0  24443  prdsbl  24520  stdbdxmet  24544  stdbdmopn  24547  metustto  24582  metustid  24583  metustexhalf  24585  cfilucfil  24588  blval2  24591  metuel2  24594  nmoge0  24750  nmo0  24764  cnblcld  24803  blssioo  24824  blcvx  24827  xrsxmet  24839  metdsf  24878  metds0  24880  metdseq0  24884  metnrmlem1a  24888  iccpnfcnv  24975  iccpnfhmeo  24976  xrhmeo  24977  pcoass  25055  iscfil2  25297  ovolmge0  25508  ovolge0  25512  ovolf  25513  ovolssnul  25518  ovolctb  25521  ovoliunnul  25538  ovolicopnf  25555  voliunlem3  25583  volsup  25587  ioorf  25604  volivth  25638  vitalilem4  25642  vitalilem5  25643  itg2ge0  25766  itg2const2  25772  itg2seq  25773  itg2monolem1  25781  itg2monolem2  25782  itg2monolem3  25783  itg2gt0  25791  dvne0  26042  mdegle0  26106  ply1remlem  26194  ply1rem  26195  idomrootle  26202  plypf1  26241  aaliou3lem2  26373  aaliou3lem3  26374  taylfvallem1  26386  taylfval  26388  tayl0  26391  radcnvcl  26446  radcnvle  26449  pserulm  26451  psercnlem1  26454  pilem2  26481  sinhalfpilem  26494  sincosq1lem  26528  sincosq1sgn  26529  sincosq2sgn  26530  tangtx  26536  tanabsge  26537  sinq12gt0  26538  cosq14gt0  26541  sincos4thpi  26544  pige3ALT  26551  cos02pilt1  26557  cosq34lt1  26558  cosordlem  26561  cos0pilt1  26563  tanord1  26568  tanord  26569  efifo  26578  argimgt0  26643  argimlt0  26644  logccv  26694  loglesqrt  26792  atantan  26954  rlimcnp  26996  rlimcnp2  26997  scvxcvx  27016  basellem1  27111  dchrisum0lem2a  27547  pntibndlem1  27619  pntibnd  27623  pntlemc  27625  pntlem3  27639  abvcxp  27645  padicabvf  27661  padicabvcxp  27662  ostth2  27667  ttgcontlem1  29020  elntg2  29121  nmooge0  30905  nmoo0  30929  nmlnogt0  30935  nmopge0  32049  nmopgt0  32050  nmfnge0  32065  nmop0  32124  nmfn0  32125  xraddge02  32898  xlt2addrd  32900  xrge0infss  32901  sgncl  32972  sgn3da  32975  elxrge02  33059  xrs0  33134  xrge00  33142  xrge0addass  33144  xrge0addgt0  33145  xrge0adddir  33146  fsumrp0cl  33149  ply1unit  33715  vietadeg1  33819  rtelextdg2lem  33967  metider  34135  unitssxrge0  34141  xrge0iifcnv  34174  xrge0iifcv  34175  xrge0iifiso  34176  xrge0iifhom  34178  xrge0mulc1cn  34182  pnfneige0  34192  lmxrge0  34193  esumgsum  34286  esumnul  34289  esum0  34290  esumle  34299  esumlef  34303  esumcst  34304  esumsnf  34305  esumpr2  34308  esumpinfval  34314  esumpinfsum  34318  esumpcvgval  34319  esumpmono  34320  hashf2  34325  esumcvg  34327  measle0  34449  voliune  34470  volfiniune  34471  ddemeas  34477  aean  34485  oms0  34538  prob01  34654  probmeasb  34671  dstfrvclim1  34719  signsply0  34792  chtvalz  34870  hgt750lemf  34894  cvmliftlem10  35582  cvmliftlem13  35584  sinccvglem  35960  dnizeq0  36851  iccioo01  37759  sin2h  38047  tan2h  38049  broucube  38091  mblfinlem2  38095  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  mbfposadd  38104  itg2addnclem2  38109  itg2gt0cn  38112  ftc1anclem5  38134  ftc1anclem8  38137  dvasin  38141  areacirc  38150  rrnequiv  38272  dvrelog2b  42621  aks6d1c5lem3  42692  aks6d1c6lem1  42725  acos1half  42905  redvmptabs  42907  readvrec2  42908  readvrec  42909  imo72b2  44686  absfico  45732  xadd0ge  45836  xrge0nemnfd  45846  xralrple2  45868  xrpnf  45997  pnfel0pnf  46042  ge0xrre  46045  sqrlearg  46067  fsumge0cl  46087  limsup10ex  46285  liminf10ex  46286  sinaover2ne0  46380  itgsin0pilem1  46462  iblsplit  46478  stoweidlem46  46558  fourierdlem43  46662  fourierdlem44  46663  fourierdlem60  46678  fourierdlem61  46679  fourierdlem87  46705  fourierdlem103  46721  fourierdlem104  46722  fourierdlem111  46729  sqwvfourb  46741  fourierswlem  46742  fouriersw  46743  etransclem23  46769  salexct2  46851  fge0npnf  46879  fge0iccico  46882  gsumge0cl  46883  sge0z  46887  sge00  46888  sge0sn  46891  sge0tsms  46892  sge0cl  46893  sge0f1o  46894  sge0ge0  46896  sge0repnf  46898  sge0fsum  46899  sge0pr  46906  sge0ssre  46909  sge0prle  46913  sge0p1  46926  sge0iunmptlemre  46927  sge0rpcpnf  46933  sge0rernmpt  46934  sge0isum  46939  sge0ad2en  46943  sge0xaddlem2  46946  sge0uzfsumgt  46956  sge0seq  46958  sge0reuz  46959  voliunsge0lem  46984  meage0  46987  meassre  46989  meale0eq0  46990  meaiuninclem  46992  omessre  47022  omeiunltfirp  47031  carageniuncllem2  47034  carageniuncl  47035  omege0  47045  omess0  47046  hoiprodcl  47059  ovnlerp  47074  ovnf  47075  ovn0lem  47077  ovnsubaddlem1  47082  hoiprodcl3  47092  hoidmvcl  47094  hoidmv1lelem3  47105  hoidmvlelem5  47111  ovnhoilem1  47113  ovolval5lem1  47164  pimrecltneg  47236  rehalfge1  47871  mod42tp1mod8  48149  eenglngeehlnmlem1  49297  eenglngeehlnmlem2  49298  rrxsphere  49308  itscnhlinecirc02p  49345  iooii  49477  io1ii  49480  sepfsepc  49487  seppcld  49489