Theorem 0xr 11337

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 11334	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11292	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 4005	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2108  ℝcr 11183  0cc0 11184  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328

This theorem is referenced by:  0lepnf  13195  ge0gtmnf  13234  max0sub  13258  xlt0neg1  13281  xlt0neg2  13282  xle0neg1  13283  xle0neg2  13284  xaddf  13286  xaddrid  13303  xaddlid  13304  xnn0xadd0  13309  xaddge0  13320  xsubge0  13323  xposdif  13324  xmullem  13326  xmullem2  13327  xmul01  13329  xmul02  13330  xmulneg1  13331  xmulf  13334  xmulpnf1  13336  xmulasslem2  13344  xmulge0  13346  xmulasslem  13347  xlemul1a  13350  xadddi  13357  xadddi2  13359  dfrp2  13456  ioopos  13484  ioorebas  13511  xrge0neqmnf  13512  elxrge0  13517  0e0iccpnf  13519  xov1plusxeqvd  13558  xnn0xrge0  13566  ico01fl0  13870  rpsup  13917  addmodid  13970  hashgt0  14437  hashle00  14449  hashgt0elex  14450  hashgt23el  14473  sgn0  15138  sgnp  15139  sgnn  15143  fprodge0  16041  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  cos1bnd  16235  sinltx  16237  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  sincos1sgn  16241  sincos2sgn  16242  halfleoddlt  16410  xrsmgm  21442  leordtval2  23241  pnfnei  23249  mnfnei  23250  psmetge0  24343  isxmet2d  24358  xmetge0  24375  xmetgt0  24389  prdsdsf  24398  prdsxmetlem  24399  xpsdsval  24412  blgt0  24430  xblss2ps  24432  xblss2  24433  xbln0  24445  prdsbl  24525  stdbdxmet  24549  stdbdmopn  24552  metustto  24587  metustid  24588  metustexhalf  24590  cfilucfil  24593  blval2  24596  metuel2  24599  nmoge0  24763  nmo0  24777  cnblcld  24816  blssioo  24836  blcvx  24839  xrsxmet  24850  metdsf  24889  metds0  24891  metdseq0  24895  metnrmlem1a  24899  iccpnfcnv  24994  iccpnfhmeo  24995  xrhmeo  24996  pcoass  25076  iscfil2  25319  ovolmge0  25531  ovolge0  25535  ovolf  25536  ovolssnul  25541  ovolctb  25544  ovoliunnul  25561  ovolicopnf  25578  voliunlem3  25606  volsup  25610  ioorf  25627  volivth  25661  vitalilem4  25665  vitalilem5  25666  itg2ge0  25790  itg2const2  25796  itg2seq  25797  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2gt0  25815  dvne0  26070  mdegle0  26136  ply1remlem  26224  ply1rem  26225  idomrootle  26232  plypf1  26271  aaliou3lem2  26403  aaliou3lem3  26404  taylfvallem1  26416  taylfval  26418  tayl0  26421  radcnvcl  26478  radcnvle  26481  pserulm  26483  psercnlem1  26487  pilem2  26514  sinhalfpilem  26523  sincosq1lem  26557  sincosq1sgn  26558  sincosq2sgn  26559  tangtx  26565  tanabsge  26566  sinq12gt0  26567  cosq14gt0  26570  sincos4thpi  26573  pige3ALT  26580  cos02pilt1  26586  cosq34lt1  26587  cosordlem  26590  cos0pilt1  26592  tanord1  26597  tanord  26598  efifo  26607  argimgt0  26672  argimlt0  26673  logccv  26723  loglesqrt  26822  atantan  26984  rlimcnp  27026  rlimcnp2  27027  scvxcvx  27047  basellem1  27142  dchrisum0lem2a  27579  pntibndlem1  27651  pntibnd  27655  pntlemc  27657  pntlem3  27671  abvcxp  27677  padicabvf  27693  padicabvcxp  27694  ostth2  27699  ttgcontlem1  28917  elntg2  29018  nmooge0  30799  nmoo0  30823  nmlnogt0  30829  nmopge0  31943  nmopgt0  31944  nmfnge0  31959  nmop0  32018  nmfn0  32019  xraddge02  32763  xlt2addrd  32765  xrge0infss  32767  elxrge02  32896  xrs0  32989  xrge00  32998  xrge0addass  33002  xrge0addgt0  33003  xrge0adddir  33004  fsumrp0cl  33007  ply1unit  33565  rtelextdg2lem  33717  metider  33840  unitssxrge0  33846  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  xrge0mulc1cn  33887  pnfneige0  33897  lmxrge0  33898  esumgsum  34009  esumnul  34012  esum0  34013  esumle  34022  esumlef  34026  esumcst  34027  esumsnf  34028  esumpr2  34031  esumpinfval  34037  esumpinfsum  34041  esumpcvgval  34042  esumpmono  34043  hashf2  34048  esumcvg  34050  measle0  34172  voliune  34193  volfiniune  34194  ddemeas  34200  aean  34208  oms0  34262  prob01  34378  probmeasb  34395  dstfrvclim1  34442  sgncl  34503  sgn3da  34506  signsply0  34528  chtvalz  34606  hgt750lemf  34630  cvmliftlem10  35262  cvmliftlem13  35264  sinccvglem  35640  dnizeq0  36441  iccioo01  37293  sin2h  37570  tan2h  37572  broucube  37614  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfposadd  37627  itg2addnclem2  37632  itg2gt0cn  37635  ftc1anclem5  37657  ftc1anclem8  37660  dvasin  37664  areacirc  37673  rrnequiv  37795  dvrelog2b  42023  aks6d1c5lem3  42094  aks6d1c6lem1  42127  acos1half  42340  imo72b2  44134  absfico  45125  xadd0ge  45235  xrge0nemnfd  45247  xralrple2  45269  xrpnf  45401  pnfel0pnf  45446  ge0xrre  45449  sqrlearg  45471  fsumge0cl  45494  limsup10ex  45694  liminf10ex  45695  sinaover2ne0  45789  itgsin0pilem1  45871  iblsplit  45887  stoweidlem46  45967  fourierdlem43  46071  fourierdlem44  46072  fourierdlem60  46087  fourierdlem61  46088  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem23  46178  salexct2  46260  fge0npnf  46288  fge0iccico  46291  gsumge0cl  46292  sge0z  46296  sge00  46297  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0ge0  46305  sge0repnf  46307  sge0fsum  46308  sge0pr  46315  sge0ssre  46318  sge0prle  46322  sge0p1  46335  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0rernmpt  46343  sge0isum  46348  sge0ad2en  46352  sge0xaddlem2  46355  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  voliunsge0lem  46393  meage0  46396  meassre  46398  meale0eq0  46399  meaiuninclem  46401  omessre  46431  omeiunltfirp  46440  carageniuncllem2  46443  carageniuncl  46444  omege0  46454  omess0  46455  hoiprodcl  46468  ovnlerp  46483  ovnf  46484  ovn0lem  46486  ovnsubaddlem1  46491  hoiprodcl3  46501  hoidmvcl  46503  hoidmv1lelem3  46514  hoidmvlelem5  46520  ovnhoilem1  46522  ovolval5lem1  46573  pimrecltneg  46645  mod42tp1mod8  47476  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrxsphere  48482  itscnhlinecirc02p  48519  iooii  48597  io1ii  48600  sepfsepc  48607  seppcld  48609