Theorem 0xr 11180

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

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

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 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 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-un 3895  df-ss 3907  df-xr 11171

This theorem is referenced by:  0lepnf  13048  ge0gtmnf  13088  max0sub  13112  xlt0neg1  13135  xlt0neg2  13136  xle0neg1  13137  xle0neg2  13138  xaddf  13140  xaddrid  13157  xaddlid  13158  xnn0xadd0  13163  xaddge0  13174  xsubge0  13177  xposdif  13178  xmullem  13180  xmullem2  13181  xmul01  13183  xmul02  13184  xmulneg1  13185  xmulf  13188  xmulpnf1  13190  xmulasslem2  13198  xmulge0  13200  xmulasslem  13201  xlemul1a  13204  xadddi  13211  xadddi2  13213  dfrp2  13311  ioopos  13341  ioorebas  13368  xrge0neqmnf  13369  elxrge0  13374  0e0iccpnf  13376  xov1plusxeqvd  13415  xnn0xrge0  13423  ico01fl0  13740  rpsup  13787  addmodid  13843  hashgt0  14312  hashle00  14324  hashgt0elex  14325  hashgt23el  14348  sgn0  15013  sgnp  15014  sgnn  15018  fprodge0  15917  ef01bndlem  16110  sin01bnd  16111  cos01bnd  16112  cos1bnd  16113  sinltx  16115  sin01gt0  16116  cos01gt0  16117  sin02gt0  16118  sincos1sgn  16119  sincos2sgn  16120  halfleoddlt  16290  xrsmgm  21363  leordtval2  23155  pnfnei  23163  mnfnei  23164  psmetge0  24255  isxmet2d  24270  xmetge0  24287  xmetgt0  24301  prdsdsf  24310  prdsxmetlem  24311  xpsdsval  24324  blgt0  24342  xblss2ps  24344  xblss2  24345  xbln0  24357  prdsbl  24434  stdbdxmet  24458  stdbdmopn  24461  metustto  24496  metustid  24497  metustexhalf  24499  cfilucfil  24502  blval2  24505  metuel2  24508  nmoge0  24664  nmo0  24678  cnblcld  24717  blssioo  24738  blcvx  24741  xrsxmet  24753  metdsf  24792  metds0  24794  metdseq0  24798  metnrmlem1a  24802  iccpnfcnv  24889  iccpnfhmeo  24890  xrhmeo  24891  pcoass  24969  iscfil2  25211  ovolmge0  25422  ovolge0  25426  ovolf  25427  ovolssnul  25432  ovolctb  25435  ovoliunnul  25452  ovolicopnf  25469  voliunlem3  25497  volsup  25501  ioorf  25518  volivth  25552  vitalilem4  25556  vitalilem5  25557  itg2ge0  25680  itg2const2  25686  itg2seq  25687  itg2monolem1  25695  itg2monolem2  25696  itg2monolem3  25697  itg2gt0  25705  dvne0  25957  mdegle0  26023  ply1remlem  26111  ply1rem  26112  idomrootle  26119  plypf1  26158  aaliou3lem2  26291  aaliou3lem3  26292  taylfvallem1  26304  taylfval  26306  tayl0  26309  radcnvcl  26366  radcnvle  26369  pserulm  26371  psercnlem1  26375  pilem2  26402  sinhalfpilem  26412  sincosq1lem  26446  sincosq1sgn  26447  sincosq2sgn  26448  tangtx  26454  tanabsge  26455  sinq12gt0  26456  cosq14gt0  26459  sincos4thpi  26462  pige3ALT  26469  cos02pilt1  26475  cosq34lt1  26476  cosordlem  26479  cos0pilt1  26481  tanord1  26486  tanord  26487  efifo  26496  argimgt0  26561  argimlt0  26562  logccv  26612  loglesqrt  26711  atantan  26873  rlimcnp  26915  rlimcnp2  26916  scvxcvx  26936  basellem1  27031  dchrisum0lem2a  27468  pntibndlem1  27540  pntibnd  27544  pntlemc  27546  pntlem3  27560  abvcxp  27566  padicabvf  27582  padicabvcxp  27583  ostth2  27588  ttgcontlem1  28941  elntg2  29042  nmooge0  30827  nmoo0  30851  nmlnogt0  30857  nmopge0  31971  nmopgt0  31972  nmfnge0  31987  nmop0  32046  nmfn0  32047  xraddge02  32820  xlt2addrd  32822  xrge0infss  32823  sgncl  32895  sgn3da  32898  elxrge02  32996  xrs0  33071  xrge00  33079  xrge0addass  33081  xrge0addgt0  33082  xrge0adddir  33083  fsumrp0cl  33086  ply1unit  33640  vietadeg1  33727  rtelextdg2lem  33876  metider  34044  unitssxrge0  34050  xrge0iifcnv  34083  xrge0iifcv  34084  xrge0iifiso  34085  xrge0iifhom  34087  xrge0mulc1cn  34091  pnfneige0  34101  lmxrge0  34102  esumgsum  34195  esumnul  34198  esum0  34199  esumle  34208  esumlef  34212  esumcst  34213  esumsnf  34214  esumpr2  34217  esumpinfval  34223  esumpinfsum  34227  esumpcvgval  34228  esumpmono  34229  hashf2  34234  esumcvg  34236  measle0  34358  voliune  34379  volfiniune  34380  ddemeas  34386  aean  34394  oms0  34447  prob01  34563  probmeasb  34580  dstfrvclim1  34628  signsply0  34701  chtvalz  34779  hgt750lemf  34803  cvmliftlem10  35482  cvmliftlem13  35484  sinccvglem  35860  dnizeq0  36733  iccioo01  37639  sin2h  37922  tan2h  37924  broucube  37966  mblfinlem2  37970  ovoliunnfl  37974  voliunnfl  37976  volsupnfl  37977  mbfposadd  37979  itg2addnclem2  37984  itg2gt0cn  37987  ftc1anclem5  38009  ftc1anclem8  38012  dvasin  38016  areacirc  38025  rrnequiv  38147  dvrelog2b  42497  aks6d1c5lem3  42568  aks6d1c6lem1  42601  acos1half  42789  redvmptabs  42791  readvrec2  42792  readvrec  42793  imo72b2  44602  absfico  45650  xadd0ge  45755  xrge0nemnfd  45765  xralrple2  45787  xrpnf  45917  pnfel0pnf  45962  ge0xrre  45965  sqrlearg  45987  fsumge0cl  46007  limsup10ex  46205  liminf10ex  46206  sinaover2ne0  46300  itgsin0pilem1  46382  iblsplit  46398  stoweidlem46  46478  fourierdlem43  46582  fourierdlem44  46583  fourierdlem60  46598  fourierdlem61  46599  fourierdlem87  46625  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  sqwvfourb  46661  fourierswlem  46662  fouriersw  46663  etransclem23  46689  salexct2  46771  fge0npnf  46799  fge0iccico  46802  gsumge0cl  46803  sge0z  46807  sge00  46808  sge0sn  46811  sge0tsms  46812  sge0cl  46813  sge0f1o  46814  sge0ge0  46816  sge0repnf  46818  sge0fsum  46819  sge0pr  46826  sge0ssre  46829  sge0prle  46833  sge0p1  46846  sge0iunmptlemre  46847  sge0rpcpnf  46853  sge0rernmpt  46854  sge0isum  46859  sge0ad2en  46863  sge0xaddlem2  46866  sge0uzfsumgt  46876  sge0seq  46878  sge0reuz  46879  voliunsge0lem  46904  meage0  46907  meassre  46909  meale0eq0  46910  meaiuninclem  46912  omessre  46942  omeiunltfirp  46951  carageniuncllem2  46954  carageniuncl  46955  omege0  46965  omess0  46966  hoiprodcl  46979  ovnlerp  46994  ovnf  46995  ovn0lem  46997  ovnsubaddlem1  47002  hoiprodcl3  47012  hoidmvcl  47014  hoidmv1lelem3  47025  hoidmvlelem5  47031  ovnhoilem1  47033  ovolval5lem1  47084  pimrecltneg  47156  rehalfge1  47769  mod42tp1mod8  48036  eenglngeehlnmlem1  49171  eenglngeehlnmlem2  49172  rrxsphere  49182  itscnhlinecirc02p  49219  iooii  49351  io1ii  49354  sepfsepc  49361  seppcld  49363