Theorem 0xr 10953

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

Syntax hints:   ∈ wcel 2108  ℝcr 10801  0cc0 10802  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944

This theorem is referenced by:  0lepnf  12797  ge0gtmnf  12835  max0sub  12859  xlt0neg1  12882  xlt0neg2  12883  xle0neg1  12884  xle0neg2  12885  xaddf  12887  xaddid1  12904  xaddid2  12905  xnn0xadd0  12910  xaddge0  12921  xsubge0  12924  xposdif  12925  xmullem  12927  xmullem2  12928  xmul01  12930  xmul02  12931  xmulneg1  12932  xmulf  12935  xmulpnf1  12937  xmulasslem2  12945  xmulge0  12947  xmulasslem  12948  xlemul1a  12951  xadddi  12958  xadddi2  12960  dfrp2  13057  ioopos  13085  ioorebas  13112  xrge0neqmnf  13113  elxrge0  13118  0e0iccpnf  13120  xov1plusxeqvd  13159  xnn0xrge0  13167  ico01fl0  13467  rpsup  13514  addmodid  13567  hashgt0  14031  hashle00  14043  hashgt0elex  14044  hashgt23el  14067  sgn0  14728  sgnp  14729  sgnn  14733  fprodge0  15631  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos1bnd  15824  sinltx  15826  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  sincos1sgn  15830  sincos2sgn  15831  halfleoddlt  15999  xrsmgm  20545  leordtval2  22271  pnfnei  22279  mnfnei  22280  psmetge0  23373  isxmet2d  23388  xmetge0  23405  xmetgt0  23419  prdsdsf  23428  prdsxmetlem  23429  xpsdsval  23442  blgt0  23460  xblss2ps  23462  xblss2  23463  xbln0  23475  prdsbl  23553  stdbdxmet  23577  stdbdmopn  23580  metustto  23615  metustid  23616  metustexhalf  23618  cfilucfil  23621  blval2  23624  metuel2  23627  nmoge0  23791  nmo0  23805  cnblcld  23844  blssioo  23864  blcvx  23867  xrsxmet  23878  metdsf  23917  metds0  23919  metdseq0  23923  metnrmlem1a  23927  iccpnfcnv  24013  iccpnfhmeo  24014  xrhmeo  24015  pcoass  24093  iscfil2  24335  ovolmge0  24546  ovolge0  24550  ovolf  24551  ovolssnul  24556  ovolctb  24559  ovoliunnul  24576  ovolicopnf  24593  voliunlem3  24621  volsup  24625  ioorf  24642  volivth  24676  vitalilem4  24680  vitalilem5  24681  itg2ge0  24805  itg2const2  24811  itg2seq  24812  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2gt0  24830  dvne0  25080  mdegle0  25147  ply1remlem  25232  ply1rem  25233  plypf1  25278  aaliou3lem2  25408  aaliou3lem3  25409  taylfvallem1  25421  taylfval  25423  tayl0  25426  radcnvcl  25481  radcnvle  25484  pserulm  25486  psercnlem1  25489  pilem2  25516  sinhalfpilem  25525  sincosq1lem  25559  sincosq1sgn  25560  sincosq2sgn  25561  tangtx  25567  tanabsge  25568  sinq12gt0  25569  cosq14gt0  25572  sincos4thpi  25575  pige3ALT  25581  cos02pilt1  25587  cosq34lt1  25588  cosordlem  25591  cos0pilt1  25593  tanord1  25598  tanord  25599  efifo  25608  argimgt0  25672  argimlt0  25673  logccv  25723  loglesqrt  25816  atantan  25978  rlimcnp  26020  rlimcnp2  26021  scvxcvx  26040  basellem1  26135  dchrisum0lem2a  26570  pntibndlem1  26642  pntibnd  26646  pntlemc  26648  pntlem3  26662  abvcxp  26668  padicabvf  26684  padicabvcxp  26685  ostth2  26690  ttgcontlem1  27155  elntg2  27256  nmooge0  29030  nmoo0  29054  nmlnogt0  29060  nmopge0  30174  nmopgt0  30175  nmfnge0  30190  nmop0  30249  nmfn0  30250  xraddge02  30981  xlt2addrd  30983  xrge0infss  30985  elxrge02  31108  xrs0  31186  xrge00  31197  xrge0addass  31201  xrge0addgt0  31202  xrge0adddir  31203  fsumrp0cl  31206  metider  31746  unitssxrge0  31752  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iifiso  31787  xrge0iifhom  31789  xrge0mulc1cn  31793  pnfneige0  31803  lmxrge0  31804  esumgsum  31913  esumnul  31916  esum0  31917  esumle  31926  esumlef  31930  esumcst  31931  esumsnf  31932  esumpr2  31935  esumpinfval  31941  esumpinfsum  31945  esumpcvgval  31946  esumpmono  31947  hashf2  31952  esumcvg  31954  measle0  32076  voliune  32097  volfiniune  32098  ddemeas  32104  aean  32112  oms0  32164  prob01  32280  probmeasb  32297  dstfrvclim1  32344  sgncl  32405  sgn3da  32408  signsply0  32430  chtvalz  32509  hgt750lemf  32533  cvmliftlem10  33156  cvmliftlem13  33158  sinccvglem  33530  dnizeq0  34582  iccioo01  35425  sin2h  35694  tan2h  35696  broucube  35738  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfposadd  35751  itg2addnclem2  35756  itg2gt0cn  35759  ftc1anclem5  35781  ftc1anclem8  35784  dvasin  35788  areacirc  35797  rrnequiv  35920  dvrelog2b  40002  acos1half  40098  idomrootle  40936  imo72b2  41672  absfico  42647  xadd0ge  42749  xrge0nemnfd  42761  xralrple2  42783  xrpnf  42916  pnfel0pnf  42956  ge0xrre  42959  sqrlearg  42981  fsumge0cl  43004  limsup10ex  43204  liminf10ex  43205  sinaover2ne0  43299  itgsin0pilem1  43381  iblsplit  43397  stoweidlem46  43477  fourierdlem43  43581  fourierdlem44  43582  fourierdlem60  43597  fourierdlem61  43598  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem23  43688  salexct2  43768  fge0npnf  43795  fge0iccico  43798  gsumge0cl  43799  sge0z  43803  sge00  43804  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0ge0  43812  sge0repnf  43814  sge0fsum  43815  sge0pr  43822  sge0ssre  43825  sge0prle  43829  sge0p1  43842  sge0iunmptlemre  43843  sge0rpcpnf  43849  sge0rernmpt  43850  sge0isum  43855  sge0ad2en  43859  sge0xaddlem2  43862  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  voliunsge0lem  43900  meage0  43903  meassre  43905  meale0eq0  43906  meaiuninclem  43908  omessre  43938  omeiunltfirp  43947  carageniuncllem2  43950  carageniuncl  43951  omege0  43961  omess0  43962  hoiprodcl  43975  ovnlerp  43990  ovnf  43991  ovn0lem  43993  ovnsubaddlem1  43998  hoiprodcl3  44008  hoidmvcl  44010  hoidmv1lelem3  44021  hoidmvlelem5  44027  ovnhoilem1  44029  ovolval5lem1  44080  pimrecltneg  44147  mod42tp1mod8  44942  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrxsphere  45982  itscnhlinecirc02p  46019  iooii  46099  io1ii  46102  sepfsepc  46109  seppcld  46111