Theorem 0xr 11260

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 11257	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11215	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3979	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2106  ℝcr 11108  0cc0 11109  ℝ^*cxr 11246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11167  ax-addrcl 11170  ax-rnegex 11180  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-xr 11251

This theorem is referenced by:  0lepnf  13111  ge0gtmnf  13150  max0sub  13174  xlt0neg1  13197  xlt0neg2  13198  xle0neg1  13199  xle0neg2  13200  xaddf  13202  xaddrid  13219  xaddlid  13220  xnn0xadd0  13225  xaddge0  13236  xsubge0  13239  xposdif  13240  xmullem  13242  xmullem2  13243  xmul01  13245  xmul02  13246  xmulneg1  13247  xmulf  13250  xmulpnf1  13252  xmulasslem2  13260  xmulge0  13262  xmulasslem  13263  xlemul1a  13266  xadddi  13273  xadddi2  13275  dfrp2  13372  ioopos  13400  ioorebas  13427  xrge0neqmnf  13428  elxrge0  13433  0e0iccpnf  13435  xov1plusxeqvd  13474  xnn0xrge0  13482  ico01fl0  13783  rpsup  13830  addmodid  13883  hashgt0  14347  hashle00  14359  hashgt0elex  14360  hashgt23el  14383  sgn0  15035  sgnp  15036  sgnn  15040  fprodge0  15936  ef01bndlem  16126  sin01bnd  16127  cos01bnd  16128  cos1bnd  16129  sinltx  16131  sin01gt0  16132  cos01gt0  16133  sin02gt0  16134  sincos1sgn  16135  sincos2sgn  16136  halfleoddlt  16304  xrsmgm  20979  leordtval2  22715  pnfnei  22723  mnfnei  22724  psmetge0  23817  isxmet2d  23832  xmetge0  23849  xmetgt0  23863  prdsdsf  23872  prdsxmetlem  23873  xpsdsval  23886  blgt0  23904  xblss2ps  23906  xblss2  23907  xbln0  23919  prdsbl  23999  stdbdxmet  24023  stdbdmopn  24026  metustto  24061  metustid  24062  metustexhalf  24064  cfilucfil  24067  blval2  24070  metuel2  24073  nmoge0  24237  nmo0  24251  cnblcld  24290  blssioo  24310  blcvx  24313  xrsxmet  24324  metdsf  24363  metds0  24365  metdseq0  24369  metnrmlem1a  24373  iccpnfcnv  24459  iccpnfhmeo  24460  xrhmeo  24461  pcoass  24539  iscfil2  24782  ovolmge0  24993  ovolge0  24997  ovolf  24998  ovolssnul  25003  ovolctb  25006  ovoliunnul  25023  ovolicopnf  25040  voliunlem3  25068  volsup  25072  ioorf  25089  volivth  25123  vitalilem4  25127  vitalilem5  25128  itg2ge0  25252  itg2const2  25258  itg2seq  25259  itg2monolem1  25267  itg2monolem2  25268  itg2monolem3  25269  itg2gt0  25277  dvne0  25527  mdegle0  25594  ply1remlem  25679  ply1rem  25680  plypf1  25725  aaliou3lem2  25855  aaliou3lem3  25856  taylfvallem1  25868  taylfval  25870  tayl0  25873  radcnvcl  25928  radcnvle  25931  pserulm  25933  psercnlem1  25936  pilem2  25963  sinhalfpilem  25972  sincosq1lem  26006  sincosq1sgn  26007  sincosq2sgn  26008  tangtx  26014  tanabsge  26015  sinq12gt0  26016  cosq14gt0  26019  sincos4thpi  26022  pige3ALT  26028  cos02pilt1  26034  cosq34lt1  26035  cosordlem  26038  cos0pilt1  26040  tanord1  26045  tanord  26046  efifo  26055  argimgt0  26119  argimlt0  26120  logccv  26170  loglesqrt  26263  atantan  26425  rlimcnp  26467  rlimcnp2  26468  scvxcvx  26487  basellem1  26582  dchrisum0lem2a  27017  pntibndlem1  27089  pntibnd  27093  pntlemc  27095  pntlem3  27109  abvcxp  27115  padicabvf  27131  padicabvcxp  27132  ostth2  27137  ttgcontlem1  28139  elntg2  28240  nmooge0  30015  nmoo0  30039  nmlnogt0  30045  nmopge0  31159  nmopgt0  31160  nmfnge0  31175  nmop0  31234  nmfn0  31235  xraddge02  31964  xlt2addrd  31966  xrge0infss  31968  elxrge02  32093  xrs0  32171  xrge00  32182  xrge0addass  32186  xrge0addgt0  32187  xrge0adddir  32188  fsumrp0cl  32191  metider  32869  unitssxrge0  32875  xrge0iifcnv  32908  xrge0iifcv  32909  xrge0iifiso  32910  xrge0iifhom  32912  xrge0mulc1cn  32916  pnfneige0  32926  lmxrge0  32927  esumgsum  33038  esumnul  33041  esum0  33042  esumle  33051  esumlef  33055  esumcst  33056  esumsnf  33057  esumpr2  33060  esumpinfval  33066  esumpinfsum  33070  esumpcvgval  33071  esumpmono  33072  hashf2  33077  esumcvg  33079  measle0  33201  voliune  33222  volfiniune  33223  ddemeas  33229  aean  33237  oms0  33291  prob01  33407  probmeasb  33424  dstfrvclim1  33471  sgncl  33532  sgn3da  33535  signsply0  33557  chtvalz  33636  hgt750lemf  33660  cvmliftlem10  34280  cvmliftlem13  34282  sinccvglem  34652  dnizeq0  35346  iccioo01  36203  sin2h  36473  tan2h  36475  broucube  36517  mblfinlem2  36521  ovoliunnfl  36525  voliunnfl  36527  volsupnfl  36528  mbfposadd  36530  itg2addnclem2  36535  itg2gt0cn  36538  ftc1anclem5  36560  ftc1anclem8  36563  dvasin  36567  areacirc  36576  rrnequiv  36698  dvrelog2b  40926  acos1half  41025  idomrootle  41927  imo72b2  42914  absfico  43907  xadd0ge  44020  xrge0nemnfd  44032  xralrple2  44054  xrpnf  44186  pnfel0pnf  44231  ge0xrre  44234  sqrlearg  44256  fsumge0cl  44279  limsup10ex  44479  liminf10ex  44480  sinaover2ne0  44574  itgsin0pilem1  44656  iblsplit  44672  stoweidlem46  44752  fourierdlem43  44856  fourierdlem44  44857  fourierdlem60  44872  fourierdlem61  44873  fourierdlem87  44899  fourierdlem103  44915  fourierdlem104  44916  fourierdlem111  44923  sqwvfourb  44935  fourierswlem  44936  fouriersw  44937  etransclem23  44963  salexct2  45045  fge0npnf  45073  fge0iccico  45076  gsumge0cl  45077  sge0z  45081  sge00  45082  sge0sn  45085  sge0tsms  45086  sge0cl  45087  sge0f1o  45088  sge0ge0  45090  sge0repnf  45092  sge0fsum  45093  sge0pr  45100  sge0ssre  45103  sge0prle  45107  sge0p1  45120  sge0iunmptlemre  45121  sge0rpcpnf  45127  sge0rernmpt  45128  sge0isum  45133  sge0ad2en  45137  sge0xaddlem2  45140  sge0uzfsumgt  45150  sge0seq  45152  sge0reuz  45153  voliunsge0lem  45178  meage0  45181  meassre  45183  meale0eq0  45184  meaiuninclem  45186  omessre  45216  omeiunltfirp  45225  carageniuncllem2  45228  carageniuncl  45229  omege0  45239  omess0  45240  hoiprodcl  45253  ovnlerp  45268  ovnf  45269  ovn0lem  45271  ovnsubaddlem1  45276  hoiprodcl3  45286  hoidmvcl  45288  hoidmv1lelem3  45299  hoidmvlelem5  45305  ovnhoilem1  45307  ovolval5lem1  45358  pimrecltneg  45430  mod42tp1mod8  46260  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  rrxsphere  47424  itscnhlinecirc02p  47461  iooii  47540  io1ii  47543  sepfsepc  47550  seppcld  47552