Theorem 0xr 10688

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 10685	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 10643	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3964	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2114  ℝcr 10536  0cc0 10537  ℝ^*cxr 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-addrcl 10598  ax-rnegex 10608  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679

This theorem is referenced by:  0lepnf  12528  ge0gtmnf  12566  max0sub  12590  xlt0neg1  12613  xlt0neg2  12614  xle0neg1  12615  xle0neg2  12616  xaddf  12618  xaddid1  12635  xaddid2  12636  xnn0xadd0  12641  xaddge0  12652  xsubge0  12655  xposdif  12656  xmullem  12658  xmullem2  12659  xmul01  12661  xmul02  12662  xmulneg1  12663  xmulf  12666  xmulpnf1  12668  xmulasslem2  12676  xmulge0  12678  xmulasslem  12679  xlemul1a  12682  xadddi  12689  xadddi2  12691  ioopos  12814  ioorebas  12840  xrge0neqmnf  12841  elxrge0  12846  0e0iccpnf  12848  xov1plusxeqvd  12885  xnn0xrge0  12892  ico01fl0  13190  rpsup  13235  addmodid  13288  hashgt0  13750  hashle00  13762  hashgt0elex  13763  hashgt23el  13786  sgn0  14448  sgnp  14449  sgnn  14453  fprodge0  15347  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  cos1bnd  15540  sinltx  15542  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  sincos1sgn  15546  sincos2sgn  15547  halfleoddlt  15711  xrsmgm  20580  leordtval2  21820  pnfnei  21828  mnfnei  21829  psmetge0  22922  isxmet2d  22937  xmetge0  22954  xmetgt0  22968  prdsdsf  22977  prdsxmetlem  22978  xpsdsval  22991  blgt0  23009  xblss2ps  23011  xblss2  23012  xbln0  23024  prdsbl  23101  stdbdxmet  23125  stdbdmopn  23128  metustto  23163  metustid  23164  metustexhalf  23166  cfilucfil  23169  blval2  23172  metuel2  23175  nmoge0  23330  nmo0  23344  cnblcld  23383  blssioo  23403  blcvx  23406  xrsxmet  23417  metdsf  23456  metds0  23458  metdseq0  23462  metnrmlem1a  23466  iccpnfcnv  23548  iccpnfhmeo  23549  xrhmeo  23550  pcoass  23628  iscfil2  23869  ovolmge0  24078  ovolge0  24082  ovolf  24083  ovolssnul  24088  ovolctb  24091  ovoliunnul  24108  ovolicopnf  24125  voliunlem3  24153  volsup  24157  ioorf  24174  volivth  24208  vitalilem4  24212  vitalilem5  24213  itg2ge0  24336  itg2const2  24342  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2gt0  24361  dvne0  24608  mdegle0  24671  ply1remlem  24756  ply1rem  24757  plypf1  24802  aaliou3lem2  24932  aaliou3lem3  24933  taylfvallem1  24945  taylfval  24947  tayl0  24950  radcnvcl  25005  radcnvle  25008  pserulm  25010  psercnlem1  25013  pilem2  25040  sinhalfpilem  25049  sincosq1lem  25083  sincosq1sgn  25084  sincosq2sgn  25085  tangtx  25091  tanabsge  25092  sinq12gt0  25093  cosq14gt0  25096  sincos4thpi  25099  pige3ALT  25105  cos02pilt1  25111  cosq34lt1  25112  cosordlem  25115  tanord1  25121  tanord  25122  efifo  25131  argimgt0  25195  argimlt0  25196  logccv  25246  loglesqrt  25339  atantan  25501  rlimcnp  25543  rlimcnp2  25544  scvxcvx  25563  basellem1  25658  dchrisum0lem2a  26093  pntibndlem1  26165  pntibnd  26169  pntlemc  26171  pntlem3  26185  abvcxp  26191  padicabvf  26207  padicabvcxp  26208  ostth2  26213  ttgcontlem1  26671  elntg2  26771  nmooge0  28544  nmoo0  28568  nmlnogt0  28574  nmopge0  29688  nmopgt0  29689  nmfnge0  29704  nmop0  29763  nmfn0  29764  xraddge02  30480  xlt2addrd  30482  xrge0infss  30484  dfrp2  30491  elxrge02  30608  xrs0  30662  xrge00  30673  xrge0addass  30677  xrge0addgt0  30678  xrge0adddir  30679  fsumrp0cl  30682  metider  31134  unitssxrge0  31143  xrge0iifcnv  31176  xrge0iifcv  31177  xrge0iifiso  31178  xrge0iifhom  31180  xrge0mulc1cn  31184  pnfneige0  31194  lmxrge0  31195  esumgsum  31304  esumnul  31307  esum0  31308  esumle  31317  esumlef  31321  esumcst  31322  esumsnf  31323  esumpr2  31326  esumpinfval  31332  esumpinfsum  31336  esumpcvgval  31337  esumpmono  31338  hashf2  31343  esumcvg  31345  measle0  31467  voliune  31488  volfiniune  31489  ddemeas  31495  aean  31503  oms0  31555  prob01  31671  probmeasb  31688  dstfrvclim1  31735  sgncl  31796  sgn3da  31799  signsply0  31821  chtvalz  31900  hgt750lemf  31924  cvmliftlem10  32541  cvmliftlem13  32543  sinccvglem  32915  dnizeq0  33814  sin2h  34897  tan2h  34899  broucube  34941  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfposadd  34954  itg2addnclem2  34959  itg2gt0cn  34962  ftc1anclem5  34986  ftc1anclem8  34989  dvasin  34993  areacirc  35002  rrnequiv  35128  idomrootle  39844  imo72b2  40574  absfico  41530  xadd0ge  41637  xrge0nemnfd  41649  xralrple2  41671  xrpnf  41811  pnfel0pnf  41853  ge0xrre  41856  sqrlearg  41878  fsumge0cl  41903  limsup10ex  42103  liminf10ex  42104  sinaover2ne0  42198  itgsin0pilem1  42284  iblsplit  42300  stoweidlem46  42380  fourierdlem43  42484  fourierdlem44  42485  fourierdlem60  42500  fourierdlem61  42501  fourierdlem87  42527  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  etransclem23  42591  salexct2  42671  fge0npnf  42698  fge0iccico  42701  gsumge0cl  42702  sge0z  42706  sge00  42707  sge0sn  42710  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0ge0  42715  sge0repnf  42717  sge0fsum  42718  sge0pr  42725  sge0ssre  42728  sge0prle  42732  sge0p1  42745  sge0iunmptlemre  42746  sge0rpcpnf  42752  sge0rernmpt  42753  sge0isum  42758  sge0ad2en  42762  sge0xaddlem2  42765  sge0uzfsumgt  42775  sge0seq  42777  sge0reuz  42778  voliunsge0lem  42803  meage0  42806  meassre  42808  meale0eq0  42809  meaiuninclem  42811  omessre  42841  omeiunltfirp  42850  carageniuncllem2  42853  carageniuncl  42854  omege0  42864  omess0  42865  hoiprodcl  42878  ovnlerp  42893  ovnf  42894  ovn0lem  42896  ovnsubaddlem1  42901  hoiprodcl3  42911  hoidmvcl  42913  hoidmv1lelem3  42924  hoidmvlelem5  42930  ovnhoilem1  42932  ovolval5lem1  42983  pimrecltneg  43050  mod42tp1mod8  43816  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrxsphere  44784  itscnhlinecirc02p  44821