Theorem 0xr 11181

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 11178	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11135	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3914	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2114  ℝcr 11026  0cc0 11027  ℝ^*cxr 11167

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 2707  ax-1cn 11085  ax-addrcl 11088  ax-rnegex 11098  ax-cnre 11100

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 2714  df-cleq 2727  df-clel 2810  df-rex 3060  df-v 3429  df-un 3890  df-ss 3902  df-xr 11172

This theorem is referenced by:  0lepnf  13073  ge0gtmnf  13113  max0sub  13137  xlt0neg1  13160  xlt0neg2  13161  xle0neg1  13162  xle0neg2  13163  xaddf  13165  xaddrid  13182  xaddlid  13183  xnn0xadd0  13188  xaddge0  13199  xsubge0  13202  xposdif  13203  xmullem  13205  xmullem2  13206  xmul01  13208  xmul02  13209  xmulneg1  13210  xmulf  13213  xmulpnf1  13215  xmulasslem2  13223  xmulge0  13225  xmulasslem  13226  xlemul1a  13229  xadddi  13236  xadddi2  13238  dfrp2  13336  ioopos  13366  ioorebas  13393  xrge0neqmnf  13394  elxrge0  13399  0e0iccpnf  13401  xov1plusxeqvd  13440  xnn0xrge0  13448  ico01fl0  13767  rpsup  13814  addmodid  13870  hashgt0  14339  hashle00  14351  hashgt0elex  14352  hashgt23el  14375  sgn0  15040  sgnp  15041  sgnn  15045  fprodge0  15947  ef01bndlem  16140  sin01bnd  16141  cos01bnd  16142  cos1bnd  16143  sinltx  16145  sin01gt0  16146  cos01gt0  16147  sin02gt0  16148  sincos1sgn  16149  sincos2sgn  16150  halfleoddlt  16320  xrsmgm  21376  leordtval2  23165  pnfnei  23173  mnfnei  23174  psmetge0  24265  isxmet2d  24280  xmetge0  24297  xmetgt0  24311  prdsdsf  24320  prdsxmetlem  24321  xpsdsval  24334  blgt0  24352  xblss2ps  24354  xblss2  24355  xbln0  24367  prdsbl  24444  stdbdxmet  24468  stdbdmopn  24471  metustto  24506  metustid  24507  metustexhalf  24509  cfilucfil  24512  blval2  24515  metuel2  24518  nmoge0  24674  nmo0  24688  cnblcld  24727  blssioo  24748  blcvx  24751  xrsxmet  24763  metdsf  24802  metds0  24804  metdseq0  24808  metnrmlem1a  24812  iccpnfcnv  24899  iccpnfhmeo  24900  xrhmeo  24901  pcoass  24979  iscfil2  25221  ovolmge0  25432  ovolge0  25436  ovolf  25437  ovolssnul  25442  ovolctb  25445  ovoliunnul  25462  ovolicopnf  25479  voliunlem3  25507  volsup  25511  ioorf  25528  volivth  25562  vitalilem4  25566  vitalilem5  25567  itg2ge0  25690  itg2const2  25696  itg2seq  25697  itg2monolem1  25705  itg2monolem2  25706  itg2monolem3  25707  itg2gt0  25715  dvne0  25966  mdegle0  26030  ply1remlem  26118  ply1rem  26119  idomrootle  26126  plypf1  26165  aaliou3lem2  26297  aaliou3lem3  26298  taylfvallem1  26310  taylfval  26312  tayl0  26315  radcnvcl  26370  radcnvle  26373  pserulm  26375  psercnlem1  26378  pilem2  26405  sinhalfpilem  26415  sincosq1lem  26449  sincosq1sgn  26450  sincosq2sgn  26451  tangtx  26457  tanabsge  26458  sinq12gt0  26459  cosq14gt0  26462  sincos4thpi  26465  pige3ALT  26472  cos02pilt1  26478  cosq34lt1  26479  cosordlem  26482  cos0pilt1  26484  tanord1  26489  tanord  26490  efifo  26499  argimgt0  26564  argimlt0  26565  logccv  26615  loglesqrt  26713  atantan  26875  rlimcnp  26917  rlimcnp2  26918  scvxcvx  26937  basellem1  27032  dchrisum0lem2a  27468  pntibndlem1  27540  pntibnd  27544  pntlemc  27546  pntlem3  27560  abvcxp  27566  padicabvf  27582  padicabvcxp  27583  ostth2  27588  ttgcontlem1  28941  elntg2  29042  nmooge0  30826  nmoo0  30850  nmlnogt0  30856  nmopge0  31970  nmopgt0  31971  nmfnge0  31986  nmop0  32045  nmfn0  32046  xraddge02  32818  xlt2addrd  32820  xrge0infss  32821  sgncl  32892  sgn3da  32895  elxrge02  32979  xrs0  33054  xrge00  33062  xrge0addass  33064  xrge0addgt0  33065  xrge0adddir  33066  fsumrp0cl  33069  ply1unit  33623  vietadeg1  33710  rtelextdg2lem  33858  metider  34026  unitssxrge0  34032  xrge0iifcnv  34065  xrge0iifcv  34066  xrge0iifiso  34067  xrge0iifhom  34069  xrge0mulc1cn  34073  pnfneige0  34083  lmxrge0  34084  esumgsum  34177  esumnul  34180  esum0  34181  esumle  34190  esumlef  34194  esumcst  34195  esumsnf  34196  esumpr2  34199  esumpinfval  34205  esumpinfsum  34209  esumpcvgval  34210  esumpmono  34211  hashf2  34216  esumcvg  34218  measle0  34340  voliune  34361  volfiniune  34362  ddemeas  34368  aean  34376  oms0  34429  prob01  34545  probmeasb  34562  dstfrvclim1  34610  signsply0  34683  chtvalz  34761  hgt750lemf  34785  cvmliftlem10  35464  cvmliftlem13  35466  sinccvglem  35842  dnizeq0  36723  iccioo01  37631  sin2h  37919  tan2h  37921  broucube  37963  mblfinlem2  37967  ovoliunnfl  37971  voliunnfl  37973  volsupnfl  37974  mbfposadd  37976  itg2addnclem2  37981  itg2gt0cn  37984  ftc1anclem5  38006  ftc1anclem8  38009  dvasin  38013  areacirc  38022  rrnequiv  38144  dvrelog2b  42493  aks6d1c5lem3  42564  aks6d1c6lem1  42597  acos1half  42778  redvmptabs  42780  readvrec2  42781  readvrec  42782  imo72b2  44587  absfico  45635  xadd0ge  45740  xrge0nemnfd  45750  xralrple2  45772  xrpnf  45901  pnfel0pnf  45946  ge0xrre  45949  sqrlearg  45971  fsumge0cl  45991  limsup10ex  46189  liminf10ex  46190  sinaover2ne0  46284  itgsin0pilem1  46366  iblsplit  46382  stoweidlem46  46462  fourierdlem43  46566  fourierdlem44  46567  fourierdlem60  46582  fourierdlem61  46583  fourierdlem87  46609  fourierdlem103  46625  fourierdlem104  46626  fourierdlem111  46633  sqwvfourb  46645  fourierswlem  46646  fouriersw  46647  etransclem23  46673  salexct2  46755  fge0npnf  46783  fge0iccico  46786  gsumge0cl  46787  sge0z  46791  sge00  46792  sge0sn  46795  sge0tsms  46796  sge0cl  46797  sge0f1o  46798  sge0ge0  46800  sge0repnf  46802  sge0fsum  46803  sge0pr  46810  sge0ssre  46813  sge0prle  46817  sge0p1  46830  sge0iunmptlemre  46831  sge0rpcpnf  46837  sge0rernmpt  46838  sge0isum  46843  sge0ad2en  46847  sge0xaddlem2  46850  sge0uzfsumgt  46860  sge0seq  46862  sge0reuz  46863  voliunsge0lem  46888  meage0  46891  meassre  46893  meale0eq0  46894  meaiuninclem  46896  omessre  46926  omeiunltfirp  46935  carageniuncllem2  46938  carageniuncl  46939  omege0  46949  omess0  46950  hoiprodcl  46963  ovnlerp  46978  ovnf  46979  ovn0lem  46981  ovnsubaddlem1  46986  hoiprodcl3  46996  hoidmvcl  46998  hoidmv1lelem3  47009  hoidmvlelem5  47015  ovnhoilem1  47017  ovolval5lem1  47068  pimrecltneg  47140  rehalfge1  47775  mod42tp1mod8  48053  eenglngeehlnmlem1  49201  eenglngeehlnmlem2  49202  rrxsphere  49212  itscnhlinecirc02p  49249  iooii  49381  io1ii  49384  sepfsepc  49391  seppcld  49393