Theorem 0xr 11267

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

Syntax hints:   ∈ wcel 2104  ℝcr 11113  0cc0 11114  ℝ^*cxr 11253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11172  ax-addrcl 11175  ax-rnegex 11185  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-v 3474  df-un 3954  df-in 3956  df-ss 3966  df-xr 11258

This theorem is referenced by:  0lepnf  13118  ge0gtmnf  13157  max0sub  13181  xlt0neg1  13204  xlt0neg2  13205  xle0neg1  13206  xle0neg2  13207  xaddf  13209  xaddrid  13226  xaddlid  13227  xnn0xadd0  13232  xaddge0  13243  xsubge0  13246  xposdif  13247  xmullem  13249  xmullem2  13250  xmul01  13252  xmul02  13253  xmulneg1  13254  xmulf  13257  xmulpnf1  13259  xmulasslem2  13267  xmulge0  13269  xmulasslem  13270  xlemul1a  13273  xadddi  13280  xadddi2  13282  dfrp2  13379  ioopos  13407  ioorebas  13434  xrge0neqmnf  13435  elxrge0  13440  0e0iccpnf  13442  xov1plusxeqvd  13481  xnn0xrge0  13489  ico01fl0  13790  rpsup  13837  addmodid  13890  hashgt0  14354  hashle00  14366  hashgt0elex  14367  hashgt23el  14390  sgn0  15042  sgnp  15043  sgnn  15047  fprodge0  15943  ef01bndlem  16133  sin01bnd  16134  cos01bnd  16135  cos1bnd  16136  sinltx  16138  sin01gt0  16139  cos01gt0  16140  sin02gt0  16141  sincos1sgn  16142  sincos2sgn  16143  halfleoddlt  16311  xrsmgm  21182  leordtval2  22938  pnfnei  22946  mnfnei  22947  psmetge0  24040  isxmet2d  24055  xmetge0  24072  xmetgt0  24086  prdsdsf  24095  prdsxmetlem  24096  xpsdsval  24109  blgt0  24127  xblss2ps  24129  xblss2  24130  xbln0  24142  prdsbl  24222  stdbdxmet  24246  stdbdmopn  24249  metustto  24284  metustid  24285  metustexhalf  24287  cfilucfil  24290  blval2  24293  metuel2  24296  nmoge0  24460  nmo0  24474  cnblcld  24513  blssioo  24533  blcvx  24536  xrsxmet  24547  metdsf  24586  metds0  24588  metdseq0  24592  metnrmlem1a  24596  iccpnfcnv  24691  iccpnfhmeo  24692  xrhmeo  24693  pcoass  24773  iscfil2  25016  ovolmge0  25228  ovolge0  25232  ovolf  25233  ovolssnul  25238  ovolctb  25241  ovoliunnul  25258  ovolicopnf  25275  voliunlem3  25303  volsup  25307  ioorf  25324  volivth  25358  vitalilem4  25362  vitalilem5  25363  itg2ge0  25487  itg2const2  25493  itg2seq  25494  itg2monolem1  25502  itg2monolem2  25503  itg2monolem3  25504  itg2gt0  25512  dvne0  25762  mdegle0  25829  ply1remlem  25914  ply1rem  25915  plypf1  25960  aaliou3lem2  26090  aaliou3lem3  26091  taylfvallem1  26103  taylfval  26105  tayl0  26108  radcnvcl  26163  radcnvle  26166  pserulm  26168  psercnlem1  26171  pilem2  26198  sinhalfpilem  26207  sincosq1lem  26241  sincosq1sgn  26242  sincosq2sgn  26243  tangtx  26249  tanabsge  26250  sinq12gt0  26251  cosq14gt0  26254  sincos4thpi  26257  pige3ALT  26263  cos02pilt1  26269  cosq34lt1  26270  cosordlem  26273  cos0pilt1  26275  tanord1  26280  tanord  26281  efifo  26290  argimgt0  26354  argimlt0  26355  logccv  26405  loglesqrt  26500  atantan  26662  rlimcnp  26704  rlimcnp2  26705  scvxcvx  26724  basellem1  26819  dchrisum0lem2a  27254  pntibndlem1  27326  pntibnd  27330  pntlemc  27332  pntlem3  27346  abvcxp  27352  padicabvf  27368  padicabvcxp  27369  ostth2  27374  ttgcontlem1  28407  elntg2  28508  nmooge0  30285  nmoo0  30309  nmlnogt0  30315  nmopge0  31429  nmopgt0  31430  nmfnge0  31445  nmop0  31504  nmfn0  31505  xraddge02  32234  xlt2addrd  32236  xrge0infss  32238  elxrge02  32363  xrs0  32441  xrge00  32452  xrge0addass  32456  xrge0addgt0  32457  xrge0adddir  32458  fsumrp0cl  32461  metider  33170  unitssxrge0  33176  xrge0iifcnv  33209  xrge0iifcv  33210  xrge0iifiso  33211  xrge0iifhom  33213  xrge0mulc1cn  33217  pnfneige0  33227  lmxrge0  33228  esumgsum  33339  esumnul  33342  esum0  33343  esumle  33352  esumlef  33356  esumcst  33357  esumsnf  33358  esumpr2  33361  esumpinfval  33367  esumpinfsum  33371  esumpcvgval  33372  esumpmono  33373  hashf2  33378  esumcvg  33380  measle0  33502  voliune  33523  volfiniune  33524  ddemeas  33530  aean  33538  oms0  33592  prob01  33708  probmeasb  33725  dstfrvclim1  33772  sgncl  33833  sgn3da  33836  signsply0  33858  chtvalz  33937  hgt750lemf  33961  cvmliftlem10  34581  cvmliftlem13  34583  sinccvglem  34953  dnizeq0  35656  iccioo01  36513  sin2h  36783  tan2h  36785  broucube  36827  mblfinlem2  36831  ovoliunnfl  36835  voliunnfl  36837  volsupnfl  36838  mbfposadd  36840  itg2addnclem2  36845  itg2gt0cn  36848  ftc1anclem5  36870  ftc1anclem8  36873  dvasin  36877  areacirc  36886  rrnequiv  37008  dvrelog2b  41239  acos1half  41719  idomrootle  42241  imo72b2  43228  absfico  44217  xadd0ge  44330  xrge0nemnfd  44342  xralrple2  44364  xrpnf  44496  pnfel0pnf  44541  ge0xrre  44544  sqrlearg  44566  fsumge0cl  44589  limsup10ex  44789  liminf10ex  44790  sinaover2ne0  44884  itgsin0pilem1  44966  iblsplit  44982  stoweidlem46  45062  fourierdlem43  45166  fourierdlem44  45167  fourierdlem60  45182  fourierdlem61  45183  fourierdlem87  45209  fourierdlem103  45225  fourierdlem104  45226  fourierdlem111  45233  sqwvfourb  45245  fourierswlem  45246  fouriersw  45247  etransclem23  45273  salexct2  45355  fge0npnf  45383  fge0iccico  45386  gsumge0cl  45387  sge0z  45391  sge00  45392  sge0sn  45395  sge0tsms  45396  sge0cl  45397  sge0f1o  45398  sge0ge0  45400  sge0repnf  45402  sge0fsum  45403  sge0pr  45410  sge0ssre  45413  sge0prle  45417  sge0p1  45430  sge0iunmptlemre  45431  sge0rpcpnf  45437  sge0rernmpt  45438  sge0isum  45443  sge0ad2en  45447  sge0xaddlem2  45450  sge0uzfsumgt  45460  sge0seq  45462  sge0reuz  45463  voliunsge0lem  45488  meage0  45491  meassre  45493  meale0eq0  45494  meaiuninclem  45496  omessre  45526  omeiunltfirp  45535  carageniuncllem2  45538  carageniuncl  45539  omege0  45549  omess0  45550  hoiprodcl  45563  ovnlerp  45578  ovnf  45579  ovn0lem  45581  ovnsubaddlem1  45586  hoiprodcl3  45596  hoidmvcl  45598  hoidmv1lelem3  45609  hoidmvlelem5  45615  ovnhoilem1  45617  ovolval5lem1  45668  pimrecltneg  45740  mod42tp1mod8  46570  eenglngeehlnmlem1  47512  eenglngeehlnmlem2  47513  rrxsphere  47523  itscnhlinecirc02p  47560  iooii  47639  io1ii  47642  sepfsepc  47649  seppcld  47651