Theorem 0xr 11221

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 11218	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11176	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3943	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2109  ℝcr 11067  0cc0 11068  ℝ^*cxr 11207

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3449  df-un 3919  df-ss 3931  df-xr 11212

This theorem is referenced by:  0lepnf  13093  ge0gtmnf  13132  max0sub  13156  xlt0neg1  13179  xlt0neg2  13180  xle0neg1  13181  xle0neg2  13182  xaddf  13184  xaddrid  13201  xaddlid  13202  xnn0xadd0  13207  xaddge0  13218  xsubge0  13221  xposdif  13222  xmullem  13224  xmullem2  13225  xmul01  13227  xmul02  13228  xmulneg1  13229  xmulf  13232  xmulpnf1  13234  xmulasslem2  13242  xmulge0  13244  xmulasslem  13245  xlemul1a  13248  xadddi  13255  xadddi2  13257  dfrp2  13355  ioopos  13385  ioorebas  13412  xrge0neqmnf  13413  elxrge0  13418  0e0iccpnf  13420  xov1plusxeqvd  13459  xnn0xrge0  13467  ico01fl0  13781  rpsup  13828  addmodid  13884  hashgt0  14353  hashle00  14365  hashgt0elex  14366  hashgt23el  14389  sgn0  15055  sgnp  15056  sgnn  15060  fprodge0  15959  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  cos1bnd  16155  sinltx  16157  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  sincos1sgn  16161  sincos2sgn  16162  halfleoddlt  16332  xrsmgm  21318  leordtval2  23099  pnfnei  23107  mnfnei  23108  psmetge0  24200  isxmet2d  24215  xmetge0  24232  xmetgt0  24246  prdsdsf  24255  prdsxmetlem  24256  xpsdsval  24269  blgt0  24287  xblss2ps  24289  xblss2  24290  xbln0  24302  prdsbl  24379  stdbdxmet  24403  stdbdmopn  24406  metustto  24441  metustid  24442  metustexhalf  24444  cfilucfil  24447  blval2  24450  metuel2  24453  nmoge0  24609  nmo0  24623  cnblcld  24662  blssioo  24683  blcvx  24686  xrsxmet  24698  metdsf  24737  metds0  24739  metdseq0  24743  metnrmlem1a  24747  iccpnfcnv  24842  iccpnfhmeo  24843  xrhmeo  24844  pcoass  24924  iscfil2  25166  ovolmge0  25378  ovolge0  25382  ovolf  25383  ovolssnul  25388  ovolctb  25391  ovoliunnul  25408  ovolicopnf  25425  voliunlem3  25453  volsup  25457  ioorf  25474  volivth  25508  vitalilem4  25512  vitalilem5  25513  itg2ge0  25636  itg2const2  25642  itg2seq  25643  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2gt0  25661  dvne0  25916  mdegle0  25982  ply1remlem  26070  ply1rem  26071  idomrootle  26078  plypf1  26117  aaliou3lem2  26251  aaliou3lem3  26252  taylfvallem1  26264  taylfval  26266  tayl0  26269  radcnvcl  26326  radcnvle  26329  pserulm  26331  psercnlem1  26335  pilem2  26362  sinhalfpilem  26372  sincosq1lem  26406  sincosq1sgn  26407  sincosq2sgn  26408  tangtx  26414  tanabsge  26415  sinq12gt0  26416  cosq14gt0  26419  sincos4thpi  26422  pige3ALT  26429  cos02pilt1  26435  cosq34lt1  26436  cosordlem  26439  cos0pilt1  26441  tanord1  26446  tanord  26447  efifo  26456  argimgt0  26521  argimlt0  26522  logccv  26572  loglesqrt  26671  atantan  26833  rlimcnp  26875  rlimcnp2  26876  scvxcvx  26896  basellem1  26991  dchrisum0lem2a  27428  pntibndlem1  27500  pntibnd  27504  pntlemc  27506  pntlem3  27520  abvcxp  27526  padicabvf  27542  padicabvcxp  27543  ostth2  27548  ttgcontlem1  28812  elntg2  28912  nmooge0  30696  nmoo0  30720  nmlnogt0  30726  nmopge0  31840  nmopgt0  31841  nmfnge0  31856  nmop0  31915  nmfn0  31916  xraddge02  32680  xlt2addrd  32682  xrge0infss  32683  sgncl  32756  sgn3da  32759  elxrge02  32852  xrs0  32944  xrge00  32953  xrge0addass  32957  xrge0addgt0  32958  xrge0adddir  32959  fsumrp0cl  32962  ply1unit  33544  rtelextdg2lem  33716  metider  33884  unitssxrge0  33890  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iifiso  33925  xrge0iifhom  33927  xrge0mulc1cn  33931  pnfneige0  33941  lmxrge0  33942  esumgsum  34035  esumnul  34038  esum0  34039  esumle  34048  esumlef  34052  esumcst  34053  esumsnf  34054  esumpr2  34057  esumpinfval  34063  esumpinfsum  34067  esumpcvgval  34068  esumpmono  34069  hashf2  34074  esumcvg  34076  measle0  34198  voliune  34219  volfiniune  34220  ddemeas  34226  aean  34234  oms0  34288  prob01  34404  probmeasb  34421  dstfrvclim1  34469  signsply0  34542  chtvalz  34620  hgt750lemf  34644  cvmliftlem10  35281  cvmliftlem13  35283  sinccvglem  35659  dnizeq0  36463  iccioo01  37315  sin2h  37604  tan2h  37606  broucube  37648  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfposadd  37661  itg2addnclem2  37666  itg2gt0cn  37669  ftc1anclem5  37691  ftc1anclem8  37694  dvasin  37698  areacirc  37707  rrnequiv  37829  dvrelog2b  42054  aks6d1c5lem3  42125  aks6d1c6lem1  42158  acos1half  42346  redvmptabs  42348  readvrec2  42349  readvrec  42350  imo72b2  44161  absfico  45212  xadd0ge  45317  xrge0nemnfd  45328  xralrple2  45350  xrpnf  45481  pnfel0pnf  45526  ge0xrre  45529  sqrlearg  45551  fsumge0cl  45571  limsup10ex  45771  liminf10ex  45772  sinaover2ne0  45866  itgsin0pilem1  45948  iblsplit  45964  stoweidlem46  46044  fourierdlem43  46148  fourierdlem44  46149  fourierdlem60  46164  fourierdlem61  46165  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem23  46255  salexct2  46337  fge0npnf  46365  fge0iccico  46368  gsumge0cl  46369  sge0z  46373  sge00  46374  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0ge0  46382  sge0repnf  46384  sge0fsum  46385  sge0pr  46392  sge0ssre  46395  sge0prle  46399  sge0p1  46412  sge0iunmptlemre  46413  sge0rpcpnf  46419  sge0rernmpt  46420  sge0isum  46425  sge0ad2en  46429  sge0xaddlem2  46432  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  voliunsge0lem  46470  meage0  46473  meassre  46475  meale0eq0  46476  meaiuninclem  46478  omessre  46508  omeiunltfirp  46517  carageniuncllem2  46520  carageniuncl  46521  omege0  46531  omess0  46532  hoiprodcl  46545  ovnlerp  46560  ovnf  46561  ovn0lem  46563  ovnsubaddlem1  46568  hoiprodcl3  46578  hoidmvcl  46580  hoidmv1lelem3  46591  hoidmvlelem5  46597  ovnhoilem1  46599  ovolval5lem1  46650  pimrecltneg  46722  rehalfge1  47336  mod42tp1mod8  47603  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrxsphere  48737  itscnhlinecirc02p  48774  iooii  48906  io1ii  48909  sepfsepc  48916  seppcld  48918