Theorem 0xr 11031

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

Syntax hints:   ∈ wcel 2107  ℝcr 10879  0cc0 10880  ℝ^*cxr 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addrcl 10941  ax-rnegex 10951  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-xr 11022

This theorem is referenced by:  0lepnf  12877  ge0gtmnf  12915  max0sub  12939  xlt0neg1  12962  xlt0neg2  12963  xle0neg1  12964  xle0neg2  12965  xaddf  12967  xaddid1  12984  xaddid2  12985  xnn0xadd0  12990  xaddge0  13001  xsubge0  13004  xposdif  13005  xmullem  13007  xmullem2  13008  xmul01  13010  xmul02  13011  xmulneg1  13012  xmulf  13015  xmulpnf1  13017  xmulasslem2  13025  xmulge0  13027  xmulasslem  13028  xlemul1a  13031  xadddi  13038  xadddi2  13040  dfrp2  13137  ioopos  13165  ioorebas  13192  xrge0neqmnf  13193  elxrge0  13198  0e0iccpnf  13200  xov1plusxeqvd  13239  xnn0xrge0  13247  ico01fl0  13548  rpsup  13595  addmodid  13648  hashgt0  14112  hashle00  14124  hashgt0elex  14125  hashgt23el  14148  sgn0  14809  sgnp  14810  sgnn  14814  fprodge0  15712  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  cos1bnd  15905  sinltx  15907  sin01gt0  15908  cos01gt0  15909  sin02gt0  15910  sincos1sgn  15911  sincos2sgn  15912  halfleoddlt  16080  xrsmgm  20642  leordtval2  22372  pnfnei  22380  mnfnei  22381  psmetge0  23474  isxmet2d  23489  xmetge0  23506  xmetgt0  23520  prdsdsf  23529  prdsxmetlem  23530  xpsdsval  23543  blgt0  23561  xblss2ps  23563  xblss2  23564  xbln0  23576  prdsbl  23656  stdbdxmet  23680  stdbdmopn  23683  metustto  23718  metustid  23719  metustexhalf  23721  cfilucfil  23724  blval2  23727  metuel2  23730  nmoge0  23894  nmo0  23908  cnblcld  23947  blssioo  23967  blcvx  23970  xrsxmet  23981  metdsf  24020  metds0  24022  metdseq0  24026  metnrmlem1a  24030  iccpnfcnv  24116  iccpnfhmeo  24117  xrhmeo  24118  pcoass  24196  iscfil2  24439  ovolmge0  24650  ovolge0  24654  ovolf  24655  ovolssnul  24660  ovolctb  24663  ovoliunnul  24680  ovolicopnf  24697  voliunlem3  24725  volsup  24729  ioorf  24746  volivth  24780  vitalilem4  24784  vitalilem5  24785  itg2ge0  24909  itg2const2  24915  itg2seq  24916  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2gt0  24934  dvne0  25184  mdegle0  25251  ply1remlem  25336  ply1rem  25337  plypf1  25382  aaliou3lem2  25512  aaliou3lem3  25513  taylfvallem1  25525  taylfval  25527  tayl0  25530  radcnvcl  25585  radcnvle  25588  pserulm  25590  psercnlem1  25593  pilem2  25620  sinhalfpilem  25629  sincosq1lem  25663  sincosq1sgn  25664  sincosq2sgn  25665  tangtx  25671  tanabsge  25672  sinq12gt0  25673  cosq14gt0  25676  sincos4thpi  25679  pige3ALT  25685  cos02pilt1  25691  cosq34lt1  25692  cosordlem  25695  cos0pilt1  25697  tanord1  25702  tanord  25703  efifo  25712  argimgt0  25776  argimlt0  25777  logccv  25827  loglesqrt  25920  atantan  26082  rlimcnp  26124  rlimcnp2  26125  scvxcvx  26144  basellem1  26239  dchrisum0lem2a  26674  pntibndlem1  26746  pntibnd  26750  pntlemc  26752  pntlem3  26766  abvcxp  26772  padicabvf  26788  padicabvcxp  26789  ostth2  26794  ttgcontlem1  27261  elntg2  27362  nmooge0  29138  nmoo0  29162  nmlnogt0  29168  nmopge0  30282  nmopgt0  30283  nmfnge0  30298  nmop0  30357  nmfn0  30358  xraddge02  31088  xlt2addrd  31090  xrge0infss  31092  elxrge02  31215  xrs0  31293  xrge00  31304  xrge0addass  31308  xrge0addgt0  31309  xrge0adddir  31310  fsumrp0cl  31313  metider  31853  unitssxrge0  31859  xrge0iifcnv  31892  xrge0iifcv  31893  xrge0iifiso  31894  xrge0iifhom  31896  xrge0mulc1cn  31900  pnfneige0  31910  lmxrge0  31911  esumgsum  32022  esumnul  32025  esum0  32026  esumle  32035  esumlef  32039  esumcst  32040  esumsnf  32041  esumpr2  32044  esumpinfval  32050  esumpinfsum  32054  esumpcvgval  32055  esumpmono  32056  hashf2  32061  esumcvg  32063  measle0  32185  voliune  32206  volfiniune  32207  ddemeas  32213  aean  32221  oms0  32273  prob01  32389  probmeasb  32406  dstfrvclim1  32453  sgncl  32514  sgn3da  32517  signsply0  32539  chtvalz  32618  hgt750lemf  32642  cvmliftlem10  33265  cvmliftlem13  33267  sinccvglem  33639  dnizeq0  34664  iccioo01  35507  sin2h  35776  tan2h  35778  broucube  35820  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  mbfposadd  35833  itg2addnclem2  35838  itg2gt0cn  35841  ftc1anclem5  35863  ftc1anclem8  35866  dvasin  35870  areacirc  35879  rrnequiv  36002  dvrelog2b  40081  acos1half  40177  idomrootle  41027  imo72b2  41790  absfico  42765  xadd0ge  42866  xrge0nemnfd  42878  xralrple2  42900  xrpnf  43033  pnfel0pnf  43073  ge0xrre  43076  sqrlearg  43098  fsumge0cl  43121  limsup10ex  43321  liminf10ex  43322  sinaover2ne0  43416  itgsin0pilem1  43498  iblsplit  43514  stoweidlem46  43594  fourierdlem43  43698  fourierdlem44  43699  fourierdlem60  43714  fourierdlem61  43715  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  etransclem23  43805  salexct2  43885  fge0npnf  43912  fge0iccico  43915  gsumge0cl  43916  sge0z  43920  sge00  43921  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0ge0  43929  sge0repnf  43931  sge0fsum  43932  sge0pr  43939  sge0ssre  43942  sge0prle  43946  sge0p1  43959  sge0iunmptlemre  43960  sge0rpcpnf  43966  sge0rernmpt  43967  sge0isum  43972  sge0ad2en  43976  sge0xaddlem2  43979  sge0uzfsumgt  43989  sge0seq  43991  sge0reuz  43992  voliunsge0lem  44017  meage0  44020  meassre  44022  meale0eq0  44023  meaiuninclem  44025  omessre  44055  omeiunltfirp  44064  carageniuncllem2  44067  carageniuncl  44068  omege0  44078  omess0  44079  hoiprodcl  44092  ovnlerp  44107  ovnf  44108  ovn0lem  44110  ovnsubaddlem1  44115  hoiprodcl3  44125  hoidmvcl  44127  hoidmv1lelem3  44138  hoidmvlelem5  44144  ovnhoilem1  44146  ovolval5lem1  44197  pimrecltneg  44269  mod42tp1mod8  45065  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrxsphere  46105  itscnhlinecirc02p  46142  iooii  46222  io1ii  46225  sepfsepc  46232  seppcld  46234