Theorem 0xr 11261

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 11258	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11216	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3980	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2107  ℝcr 11109  0cc0 11110  ℝ^*cxr 11247

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 2704  ax-1cn 11168  ax-addrcl 11171  ax-rnegex 11181  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252

This theorem is referenced by:  0lepnf  13112  ge0gtmnf  13151  max0sub  13175  xlt0neg1  13198  xlt0neg2  13199  xle0neg1  13200  xle0neg2  13201  xaddf  13203  xaddrid  13220  xaddlid  13221  xnn0xadd0  13226  xaddge0  13237  xsubge0  13240  xposdif  13241  xmullem  13243  xmullem2  13244  xmul01  13246  xmul02  13247  xmulneg1  13248  xmulf  13251  xmulpnf1  13253  xmulasslem2  13261  xmulge0  13263  xmulasslem  13264  xlemul1a  13267  xadddi  13274  xadddi2  13276  dfrp2  13373  ioopos  13401  ioorebas  13428  xrge0neqmnf  13429  elxrge0  13434  0e0iccpnf  13436  xov1plusxeqvd  13475  xnn0xrge0  13483  ico01fl0  13784  rpsup  13831  addmodid  13884  hashgt0  14348  hashle00  14360  hashgt0elex  14361  hashgt23el  14384  sgn0  15036  sgnp  15037  sgnn  15041  fprodge0  15937  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  cos1bnd  16130  sinltx  16132  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  sincos1sgn  16136  sincos2sgn  16137  halfleoddlt  16305  xrsmgm  20980  leordtval2  22716  pnfnei  22724  mnfnei  22725  psmetge0  23818  isxmet2d  23833  xmetge0  23850  xmetgt0  23864  prdsdsf  23873  prdsxmetlem  23874  xpsdsval  23887  blgt0  23905  xblss2ps  23907  xblss2  23908  xbln0  23920  prdsbl  24000  stdbdxmet  24024  stdbdmopn  24027  metustto  24062  metustid  24063  metustexhalf  24065  cfilucfil  24068  blval2  24071  metuel2  24074  nmoge0  24238  nmo0  24252  cnblcld  24291  blssioo  24311  blcvx  24314  xrsxmet  24325  metdsf  24364  metds0  24366  metdseq0  24370  metnrmlem1a  24374  iccpnfcnv  24460  iccpnfhmeo  24461  xrhmeo  24462  pcoass  24540  iscfil2  24783  ovolmge0  24994  ovolge0  24998  ovolf  24999  ovolssnul  25004  ovolctb  25007  ovoliunnul  25024  ovolicopnf  25041  voliunlem3  25069  volsup  25073  ioorf  25090  volivth  25124  vitalilem4  25128  vitalilem5  25129  itg2ge0  25253  itg2const2  25259  itg2seq  25260  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2gt0  25278  dvne0  25528  mdegle0  25595  ply1remlem  25680  ply1rem  25681  plypf1  25726  aaliou3lem2  25856  aaliou3lem3  25857  taylfvallem1  25869  taylfval  25871  tayl0  25874  radcnvcl  25929  radcnvle  25932  pserulm  25934  psercnlem1  25937  pilem2  25964  sinhalfpilem  25973  sincosq1lem  26007  sincosq1sgn  26008  sincosq2sgn  26009  tangtx  26015  tanabsge  26016  sinq12gt0  26017  cosq14gt0  26020  sincos4thpi  26023  pige3ALT  26029  cos02pilt1  26035  cosq34lt1  26036  cosordlem  26039  cos0pilt1  26041  tanord1  26046  tanord  26047  efifo  26056  argimgt0  26120  argimlt0  26121  logccv  26171  loglesqrt  26266  atantan  26428  rlimcnp  26470  rlimcnp2  26471  scvxcvx  26490  basellem1  26585  dchrisum0lem2a  27020  pntibndlem1  27092  pntibnd  27096  pntlemc  27098  pntlem3  27112  abvcxp  27118  padicabvf  27134  padicabvcxp  27135  ostth2  27140  ttgcontlem1  28142  elntg2  28243  nmooge0  30020  nmoo0  30044  nmlnogt0  30050  nmopge0  31164  nmopgt0  31165  nmfnge0  31180  nmop0  31239  nmfn0  31240  xraddge02  31969  xlt2addrd  31971  xrge0infss  31973  elxrge02  32098  xrs0  32176  xrge00  32187  xrge0addass  32191  xrge0addgt0  32192  xrge0adddir  32193  fsumrp0cl  32196  metider  32874  unitssxrge0  32880  xrge0iifcnv  32913  xrge0iifcv  32914  xrge0iifiso  32915  xrge0iifhom  32917  xrge0mulc1cn  32921  pnfneige0  32931  lmxrge0  32932  esumgsum  33043  esumnul  33046  esum0  33047  esumle  33056  esumlef  33060  esumcst  33061  esumsnf  33062  esumpr2  33065  esumpinfval  33071  esumpinfsum  33075  esumpcvgval  33076  esumpmono  33077  hashf2  33082  esumcvg  33084  measle0  33206  voliune  33227  volfiniune  33228  ddemeas  33234  aean  33242  oms0  33296  prob01  33412  probmeasb  33429  dstfrvclim1  33476  sgncl  33537  sgn3da  33540  signsply0  33562  chtvalz  33641  hgt750lemf  33665  cvmliftlem10  34285  cvmliftlem13  34287  sinccvglem  34657  dnizeq0  35351  iccioo01  36208  sin2h  36478  tan2h  36480  broucube  36522  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfposadd  36535  itg2addnclem2  36540  itg2gt0cn  36543  ftc1anclem5  36565  ftc1anclem8  36568  dvasin  36572  areacirc  36581  rrnequiv  36703  dvrelog2b  40931  acos1half  41415  idomrootle  41937  imo72b2  42924  absfico  43917  xadd0ge  44030  xrge0nemnfd  44042  xralrple2  44064  xrpnf  44196  pnfel0pnf  44241  ge0xrre  44244  sqrlearg  44266  fsumge0cl  44289  limsup10ex  44489  liminf10ex  44490  sinaover2ne0  44584  itgsin0pilem1  44666  iblsplit  44682  stoweidlem46  44762  fourierdlem43  44866  fourierdlem44  44867  fourierdlem60  44882  fourierdlem61  44883  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  etransclem23  44973  salexct2  45055  fge0npnf  45083  fge0iccico  45086  gsumge0cl  45087  sge0z  45091  sge00  45092  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0ge0  45100  sge0repnf  45102  sge0fsum  45103  sge0pr  45110  sge0ssre  45113  sge0prle  45117  sge0p1  45130  sge0iunmptlemre  45131  sge0rpcpnf  45137  sge0rernmpt  45138  sge0isum  45143  sge0ad2en  45147  sge0xaddlem2  45150  sge0uzfsumgt  45160  sge0seq  45162  sge0reuz  45163  voliunsge0lem  45188  meage0  45191  meassre  45193  meale0eq0  45194  meaiuninclem  45196  omessre  45226  omeiunltfirp  45235  carageniuncllem2  45238  carageniuncl  45239  omege0  45249  omess0  45250  hoiprodcl  45263  ovnlerp  45278  ovnf  45279  ovn0lem  45281  ovnsubaddlem1  45286  hoiprodcl3  45296  hoidmvcl  45298  hoidmv1lelem3  45309  hoidmvlelem5  45315  ovnhoilem1  45317  ovolval5lem1  45368  pimrecltneg  45440  mod42tp1mod8  46270  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrxsphere  47434  itscnhlinecirc02p  47471  iooii  47550  io1ii  47553  sepfsepc  47560  seppcld  47562