Theorem 0xr 11192

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 11189	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11146	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3919	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2114  ℝcr 11037  0cc0 11038  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-un 3895  df-ss 3907  df-xr 11183

This theorem is referenced by:  0lepnf  13084  ge0gtmnf  13124  max0sub  13148  xlt0neg1  13171  xlt0neg2  13172  xle0neg1  13173  xle0neg2  13174  xaddf  13176  xaddrid  13193  xaddlid  13194  xnn0xadd0  13199  xaddge0  13210  xsubge0  13213  xposdif  13214  xmullem  13216  xmullem2  13217  xmul01  13219  xmul02  13220  xmulneg1  13221  xmulf  13224  xmulpnf1  13226  xmulasslem2  13234  xmulge0  13236  xmulasslem  13237  xlemul1a  13240  xadddi  13247  xadddi2  13249  dfrp2  13347  ioopos  13377  ioorebas  13404  xrge0neqmnf  13405  elxrge0  13410  0e0iccpnf  13412  xov1plusxeqvd  13451  xnn0xrge0  13459  ico01fl0  13778  rpsup  13825  addmodid  13881  hashgt0  14350  hashle00  14362  hashgt0elex  14363  hashgt23el  14386  sgn0  15051  sgnp  15052  sgnn  15056  fprodge0  15958  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos1bnd  16154  sinltx  16156  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  sincos1sgn  16160  sincos2sgn  16161  halfleoddlt  16331  xrsmgm  21387  leordtval2  23177  pnfnei  23185  mnfnei  23186  psmetge0  24277  isxmet2d  24292  xmetge0  24309  xmetgt0  24323  prdsdsf  24332  prdsxmetlem  24333  xpsdsval  24346  blgt0  24364  xblss2ps  24366  xblss2  24367  xbln0  24379  prdsbl  24456  stdbdxmet  24480  stdbdmopn  24483  metustto  24518  metustid  24519  metustexhalf  24521  cfilucfil  24524  blval2  24527  metuel2  24530  nmoge0  24686  nmo0  24700  cnblcld  24739  blssioo  24760  blcvx  24763  xrsxmet  24775  metdsf  24814  metds0  24816  metdseq0  24820  metnrmlem1a  24824  iccpnfcnv  24911  iccpnfhmeo  24912  xrhmeo  24913  pcoass  24991  iscfil2  25233  ovolmge0  25444  ovolge0  25448  ovolf  25449  ovolssnul  25454  ovolctb  25457  ovoliunnul  25474  ovolicopnf  25491  voliunlem3  25519  volsup  25523  ioorf  25540  volivth  25574  vitalilem4  25578  vitalilem5  25579  itg2ge0  25702  itg2const2  25708  itg2seq  25709  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2gt0  25727  dvne0  25978  mdegle0  26042  ply1remlem  26130  ply1rem  26131  idomrootle  26138  plypf1  26177  aaliou3lem2  26309  aaliou3lem3  26310  taylfvallem1  26322  taylfval  26324  tayl0  26327  radcnvcl  26382  radcnvle  26385  pserulm  26387  psercnlem1  26390  pilem2  26417  sinhalfpilem  26427  sincosq1lem  26461  sincosq1sgn  26462  sincosq2sgn  26463  tangtx  26469  tanabsge  26470  sinq12gt0  26471  cosq14gt0  26474  sincos4thpi  26477  pige3ALT  26484  cos02pilt1  26490  cosq34lt1  26491  cosordlem  26494  cos0pilt1  26496  tanord1  26501  tanord  26502  efifo  26511  argimgt0  26576  argimlt0  26577  logccv  26627  loglesqrt  26725  atantan  26887  rlimcnp  26929  rlimcnp2  26930  scvxcvx  26949  basellem1  27044  dchrisum0lem2a  27480  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  pntlem3  27572  abvcxp  27578  padicabvf  27594  padicabvcxp  27595  ostth2  27600  ttgcontlem1  28953  elntg2  29054  nmooge0  30838  nmoo0  30862  nmlnogt0  30868  nmopge0  31982  nmopgt0  31983  nmfnge0  31998  nmop0  32057  nmfn0  32058  xraddge02  32830  xlt2addrd  32832  xrge0infss  32833  sgncl  32904  sgn3da  32907  elxrge02  32991  xrs0  33066  xrge00  33074  xrge0addass  33076  xrge0addgt0  33077  xrge0adddir  33078  fsumrp0cl  33081  ply1unit  33635  vietadeg1  33722  rtelextdg2lem  33870  metider  34038  unitssxrge0  34044  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  xrge0mulc1cn  34085  pnfneige0  34095  lmxrge0  34096  esumgsum  34189  esumnul  34192  esum0  34193  esumle  34202  esumlef  34206  esumcst  34207  esumsnf  34208  esumpr2  34211  esumpinfval  34217  esumpinfsum  34221  esumpcvgval  34222  esumpmono  34223  hashf2  34228  esumcvg  34230  measle0  34352  voliune  34373  volfiniune  34374  ddemeas  34380  aean  34388  oms0  34441  prob01  34557  probmeasb  34574  dstfrvclim1  34622  signsply0  34695  chtvalz  34773  hgt750lemf  34797  cvmliftlem10  35476  cvmliftlem13  35478  sinccvglem  35854  dnizeq0  36735  iccioo01  37643  sin2h  37931  tan2h  37933  broucube  37975  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfposadd  37988  itg2addnclem2  37993  itg2gt0cn  37996  ftc1anclem5  38018  ftc1anclem8  38021  dvasin  38025  areacirc  38034  rrnequiv  38156  dvrelog2b  42505  aks6d1c5lem3  42576  aks6d1c6lem1  42609  acos1half  42790  redvmptabs  42792  readvrec2  42793  readvrec  42794  imo72b2  44599  absfico  45647  xadd0ge  45752  xrge0nemnfd  45762  xralrple2  45784  xrpnf  45913  pnfel0pnf  45958  ge0xrre  45961  sqrlearg  45983  fsumge0cl  46003  limsup10ex  46201  liminf10ex  46202  sinaover2ne0  46296  itgsin0pilem1  46378  iblsplit  46394  stoweidlem46  46474  fourierdlem43  46578  fourierdlem44  46579  fourierdlem60  46594  fourierdlem61  46595  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem23  46685  salexct2  46767  fge0npnf  46795  fge0iccico  46798  gsumge0cl  46799  sge0z  46803  sge00  46804  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0ge0  46812  sge0repnf  46814  sge0fsum  46815  sge0pr  46822  sge0ssre  46825  sge0prle  46829  sge0p1  46842  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0rernmpt  46850  sge0isum  46855  sge0ad2en  46859  sge0xaddlem2  46862  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  voliunsge0lem  46900  meage0  46903  meassre  46905  meale0eq0  46906  meaiuninclem  46908  omessre  46938  omeiunltfirp  46947  carageniuncllem2  46950  carageniuncl  46951  omege0  46961  omess0  46962  hoiprodcl  46975  ovnlerp  46990  ovnf  46991  ovn0lem  46993  ovnsubaddlem1  46998  hoiprodcl3  47008  hoidmvcl  47010  hoidmv1lelem3  47021  hoidmvlelem5  47027  ovnhoilem1  47029  ovolval5lem1  47080  pimrecltneg  47152  rehalfge1  47781  mod42tp1mod8  48059  eenglngeehlnmlem1  49207  eenglngeehlnmlem2  49208  rrxsphere  49218  itscnhlinecirc02p  49255  iooii  49387  io1ii  49390  sepfsepc  49397  seppcld  49399