Theorem 0xr 11169

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 11166	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11124	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3928	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2113  ℝcr 11015  0cc0 11016  ℝ^*cxr 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11074  ax-addrcl 11077  ax-rnegex 11087  ax-cnre 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3059  df-v 3440  df-un 3904  df-ss 3916  df-xr 11160

This theorem is referenced by:  0lepnf  13042  ge0gtmnf  13081  max0sub  13105  xlt0neg1  13128  xlt0neg2  13129  xle0neg1  13130  xle0neg2  13131  xaddf  13133  xaddrid  13150  xaddlid  13151  xnn0xadd0  13156  xaddge0  13167  xsubge0  13170  xposdif  13171  xmullem  13173  xmullem2  13174  xmul01  13176  xmul02  13177  xmulneg1  13178  xmulf  13181  xmulpnf1  13183  xmulasslem2  13191  xmulge0  13193  xmulasslem  13194  xlemul1a  13197  xadddi  13204  xadddi2  13206  dfrp2  13304  ioopos  13334  ioorebas  13361  xrge0neqmnf  13362  elxrge0  13367  0e0iccpnf  13369  xov1plusxeqvd  13408  xnn0xrge0  13416  ico01fl0  13733  rpsup  13780  addmodid  13836  hashgt0  14305  hashle00  14317  hashgt0elex  14318  hashgt23el  14341  sgn0  15006  sgnp  15007  sgnn  15011  fprodge0  15910  ef01bndlem  16103  sin01bnd  16104  cos01bnd  16105  cos1bnd  16106  sinltx  16108  sin01gt0  16109  cos01gt0  16110  sin02gt0  16111  sincos1sgn  16112  sincos2sgn  16113  halfleoddlt  16283  xrsmgm  21353  leordtval2  23137  pnfnei  23145  mnfnei  23146  psmetge0  24237  isxmet2d  24252  xmetge0  24269  xmetgt0  24283  prdsdsf  24292  prdsxmetlem  24293  xpsdsval  24306  blgt0  24324  xblss2ps  24326  xblss2  24327  xbln0  24339  prdsbl  24416  stdbdxmet  24440  stdbdmopn  24443  metustto  24478  metustid  24479  metustexhalf  24481  cfilucfil  24484  blval2  24487  metuel2  24490  nmoge0  24646  nmo0  24660  cnblcld  24699  blssioo  24720  blcvx  24723  xrsxmet  24735  metdsf  24774  metds0  24776  metdseq0  24780  metnrmlem1a  24784  iccpnfcnv  24879  iccpnfhmeo  24880  xrhmeo  24881  pcoass  24961  iscfil2  25203  ovolmge0  25415  ovolge0  25419  ovolf  25420  ovolssnul  25425  ovolctb  25428  ovoliunnul  25445  ovolicopnf  25462  voliunlem3  25490  volsup  25494  ioorf  25511  volivth  25545  vitalilem4  25549  vitalilem5  25550  itg2ge0  25673  itg2const2  25679  itg2seq  25680  itg2monolem1  25688  itg2monolem2  25689  itg2monolem3  25690  itg2gt0  25698  dvne0  25953  mdegle0  26019  ply1remlem  26107  ply1rem  26108  idomrootle  26115  plypf1  26154  aaliou3lem2  26288  aaliou3lem3  26289  taylfvallem1  26301  taylfval  26303  tayl0  26306  radcnvcl  26363  radcnvle  26366  pserulm  26368  psercnlem1  26372  pilem2  26399  sinhalfpilem  26409  sincosq1lem  26443  sincosq1sgn  26444  sincosq2sgn  26445  tangtx  26451  tanabsge  26452  sinq12gt0  26453  cosq14gt0  26456  sincos4thpi  26459  pige3ALT  26466  cos02pilt1  26472  cosq34lt1  26473  cosordlem  26476  cos0pilt1  26478  tanord1  26483  tanord  26484  efifo  26493  argimgt0  26558  argimlt0  26559  logccv  26609  loglesqrt  26708  atantan  26870  rlimcnp  26912  rlimcnp2  26913  scvxcvx  26933  basellem1  27028  dchrisum0lem2a  27465  pntibndlem1  27537  pntibnd  27541  pntlemc  27543  pntlem3  27557  abvcxp  27563  padicabvf  27579  padicabvcxp  27580  ostth2  27585  ttgcontlem1  28873  elntg2  28974  nmooge0  30758  nmoo0  30782  nmlnogt0  30788  nmopge0  31902  nmopgt0  31903  nmfnge0  31918  nmop0  31977  nmfn0  31978  xraddge02  32751  xlt2addrd  32753  xrge0infss  32754  sgncl  32825  sgn3da  32828  elxrge02  32923  xrs0  32998  xrge00  33006  xrge0addass  33008  xrge0addgt0  33009  xrge0adddir  33010  fsumrp0cl  33013  ply1unit  33549  rtelextdg2lem  33750  metider  33918  unitssxrge0  33924  xrge0iifcnv  33957  xrge0iifcv  33958  xrge0iifiso  33959  xrge0iifhom  33961  xrge0mulc1cn  33965  pnfneige0  33975  lmxrge0  33976  esumgsum  34069  esumnul  34072  esum0  34073  esumle  34082  esumlef  34086  esumcst  34087  esumsnf  34088  esumpr2  34091  esumpinfval  34097  esumpinfsum  34101  esumpcvgval  34102  esumpmono  34103  hashf2  34108  esumcvg  34110  measle0  34232  voliune  34253  volfiniune  34254  ddemeas  34260  aean  34268  oms0  34321  prob01  34437  probmeasb  34454  dstfrvclim1  34502  signsply0  34575  chtvalz  34653  hgt750lemf  34677  cvmliftlem10  35349  cvmliftlem13  35351  sinccvglem  35727  dnizeq0  36530  iccioo01  37382  sin2h  37660  tan2h  37662  broucube  37704  mblfinlem2  37708  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  mbfposadd  37717  itg2addnclem2  37722  itg2gt0cn  37725  ftc1anclem5  37747  ftc1anclem8  37750  dvasin  37754  areacirc  37763  rrnequiv  37885  dvrelog2b  42169  aks6d1c5lem3  42240  aks6d1c6lem1  42273  acos1half  42466  redvmptabs  42468  readvrec2  42469  readvrec  42470  imo72b2  44279  absfico  45329  xadd0ge  45434  xrge0nemnfd  45445  xralrple2  45467  xrpnf  45597  pnfel0pnf  45642  ge0xrre  45645  sqrlearg  45667  fsumge0cl  45687  limsup10ex  45885  liminf10ex  45886  sinaover2ne0  45980  itgsin0pilem1  46062  iblsplit  46078  stoweidlem46  46158  fourierdlem43  46262  fourierdlem44  46263  fourierdlem60  46278  fourierdlem61  46279  fourierdlem87  46305  fourierdlem103  46321  fourierdlem104  46322  fourierdlem111  46329  sqwvfourb  46341  fourierswlem  46342  fouriersw  46343  etransclem23  46369  salexct2  46451  fge0npnf  46479  fge0iccico  46482  gsumge0cl  46483  sge0z  46487  sge00  46488  sge0sn  46491  sge0tsms  46492  sge0cl  46493  sge0f1o  46494  sge0ge0  46496  sge0repnf  46498  sge0fsum  46499  sge0pr  46506  sge0ssre  46509  sge0prle  46513  sge0p1  46526  sge0iunmptlemre  46527  sge0rpcpnf  46533  sge0rernmpt  46534  sge0isum  46539  sge0ad2en  46543  sge0xaddlem2  46546  sge0uzfsumgt  46556  sge0seq  46558  sge0reuz  46559  voliunsge0lem  46584  meage0  46587  meassre  46589  meale0eq0  46590  meaiuninclem  46592  omessre  46622  omeiunltfirp  46631  carageniuncllem2  46634  carageniuncl  46635  omege0  46645  omess0  46646  hoiprodcl  46659  ovnlerp  46674  ovnf  46675  ovn0lem  46677  ovnsubaddlem1  46682  hoiprodcl3  46692  hoidmvcl  46694  hoidmv1lelem3  46705  hoidmvlelem5  46711  ovnhoilem1  46713  ovolval5lem1  46764  pimrecltneg  46836  rehalfge1  47449  mod42tp1mod8  47716  eenglngeehlnmlem1  48852  eenglngeehlnmlem2  48853  rrxsphere  48863  itscnhlinecirc02p  48900  iooii  49032  io1ii  49035  sepfsepc  49042  seppcld  49044