Theorem 0xr 11308

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

Syntax hints:   ∈ wcel 2108  ℝcr 11154  0cc0 11155  ℝ^*cxr 11294

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addrcl 11216  ax-rnegex 11226  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299

This theorem is referenced by:  0lepnf  13175  ge0gtmnf  13214  max0sub  13238  xlt0neg1  13261  xlt0neg2  13262  xle0neg1  13263  xle0neg2  13264  xaddf  13266  xaddrid  13283  xaddlid  13284  xnn0xadd0  13289  xaddge0  13300  xsubge0  13303  xposdif  13304  xmullem  13306  xmullem2  13307  xmul01  13309  xmul02  13310  xmulneg1  13311  xmulf  13314  xmulpnf1  13316  xmulasslem2  13324  xmulge0  13326  xmulasslem  13327  xlemul1a  13330  xadddi  13337  xadddi2  13339  dfrp2  13436  ioopos  13464  ioorebas  13491  xrge0neqmnf  13492  elxrge0  13497  0e0iccpnf  13499  xov1plusxeqvd  13538  xnn0xrge0  13546  ico01fl0  13859  rpsup  13906  addmodid  13960  hashgt0  14427  hashle00  14439  hashgt0elex  14440  hashgt23el  14463  sgn0  15128  sgnp  15129  sgnn  15133  fprodge0  16029  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  cos1bnd  16223  sinltx  16225  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  sincos1sgn  16229  sincos2sgn  16230  halfleoddlt  16399  xrsmgm  21419  leordtval2  23220  pnfnei  23228  mnfnei  23229  psmetge0  24322  isxmet2d  24337  xmetge0  24354  xmetgt0  24368  prdsdsf  24377  prdsxmetlem  24378  xpsdsval  24391  blgt0  24409  xblss2ps  24411  xblss2  24412  xbln0  24424  prdsbl  24504  stdbdxmet  24528  stdbdmopn  24531  metustto  24566  metustid  24567  metustexhalf  24569  cfilucfil  24572  blval2  24575  metuel2  24578  nmoge0  24742  nmo0  24756  cnblcld  24795  blssioo  24816  blcvx  24819  xrsxmet  24831  metdsf  24870  metds0  24872  metdseq0  24876  metnrmlem1a  24880  iccpnfcnv  24975  iccpnfhmeo  24976  xrhmeo  24977  pcoass  25057  iscfil2  25300  ovolmge0  25512  ovolge0  25516  ovolf  25517  ovolssnul  25522  ovolctb  25525  ovoliunnul  25542  ovolicopnf  25559  voliunlem3  25587  volsup  25591  ioorf  25608  volivth  25642  vitalilem4  25646  vitalilem5  25647  itg2ge0  25770  itg2const2  25776  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2gt0  25795  dvne0  26050  mdegle0  26116  ply1remlem  26204  ply1rem  26205  idomrootle  26212  plypf1  26251  aaliou3lem2  26385  aaliou3lem3  26386  taylfvallem1  26398  taylfval  26400  tayl0  26403  radcnvcl  26460  radcnvle  26463  pserulm  26465  psercnlem1  26469  pilem2  26496  sinhalfpilem  26505  sincosq1lem  26539  sincosq1sgn  26540  sincosq2sgn  26541  tangtx  26547  tanabsge  26548  sinq12gt0  26549  cosq14gt0  26552  sincos4thpi  26555  pige3ALT  26562  cos02pilt1  26568  cosq34lt1  26569  cosordlem  26572  cos0pilt1  26574  tanord1  26579  tanord  26580  efifo  26589  argimgt0  26654  argimlt0  26655  logccv  26705  loglesqrt  26804  atantan  26966  rlimcnp  27008  rlimcnp2  27009  scvxcvx  27029  basellem1  27124  dchrisum0lem2a  27561  pntibndlem1  27633  pntibnd  27637  pntlemc  27639  pntlem3  27653  abvcxp  27659  padicabvf  27675  padicabvcxp  27676  ostth2  27681  ttgcontlem1  28899  elntg2  29000  nmooge0  30786  nmoo0  30810  nmlnogt0  30816  nmopge0  31930  nmopgt0  31931  nmfnge0  31946  nmop0  32005  nmfn0  32006  xraddge02  32760  xlt2addrd  32762  xrge0infss  32764  elxrge02  32914  xrs0  33008  xrge00  33017  xrge0addass  33021  xrge0addgt0  33022  xrge0adddir  33023  fsumrp0cl  33026  ply1unit  33600  rtelextdg2lem  33767  metider  33893  unitssxrge0  33899  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  xrge0mulc1cn  33940  pnfneige0  33950  lmxrge0  33951  esumgsum  34046  esumnul  34049  esum0  34050  esumle  34059  esumlef  34063  esumcst  34064  esumsnf  34065  esumpr2  34068  esumpinfval  34074  esumpinfsum  34078  esumpcvgval  34079  esumpmono  34080  hashf2  34085  esumcvg  34087  measle0  34209  voliune  34230  volfiniune  34231  ddemeas  34237  aean  34245  oms0  34299  prob01  34415  probmeasb  34432  dstfrvclim1  34480  sgncl  34541  sgn3da  34544  signsply0  34566  chtvalz  34644  hgt750lemf  34668  cvmliftlem10  35299  cvmliftlem13  35301  sinccvglem  35677  dnizeq0  36476  iccioo01  37328  sin2h  37617  tan2h  37619  broucube  37661  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfposadd  37674  itg2addnclem2  37679  itg2gt0cn  37682  ftc1anclem5  37704  ftc1anclem8  37707  dvasin  37711  areacirc  37720  rrnequiv  37842  dvrelog2b  42067  aks6d1c5lem3  42138  aks6d1c6lem1  42171  acos1half  42388  redvmptabs  42390  readvrec2  42391  readvrec  42392  imo72b2  44185  absfico  45223  xadd0ge  45332  xrge0nemnfd  45343  xralrple2  45365  xrpnf  45496  pnfel0pnf  45541  ge0xrre  45544  sqrlearg  45566  fsumge0cl  45588  limsup10ex  45788  liminf10ex  45789  sinaover2ne0  45883  itgsin0pilem1  45965  iblsplit  45981  stoweidlem46  46061  fourierdlem43  46165  fourierdlem44  46166  fourierdlem60  46181  fourierdlem61  46182  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem23  46272  salexct2  46354  fge0npnf  46382  fge0iccico  46385  gsumge0cl  46386  sge0z  46390  sge00  46391  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0ge0  46399  sge0repnf  46401  sge0fsum  46402  sge0pr  46409  sge0ssre  46412  sge0prle  46416  sge0p1  46429  sge0iunmptlemre  46430  sge0rpcpnf  46436  sge0rernmpt  46437  sge0isum  46442  sge0ad2en  46446  sge0xaddlem2  46449  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  voliunsge0lem  46487  meage0  46490  meassre  46492  meale0eq0  46493  meaiuninclem  46495  omessre  46525  omeiunltfirp  46534  carageniuncllem2  46537  carageniuncl  46538  omege0  46548  omess0  46549  hoiprodcl  46562  ovnlerp  46577  ovnf  46578  ovn0lem  46580  ovnsubaddlem1  46585  hoiprodcl3  46595  hoidmvcl  46597  hoidmv1lelem3  46608  hoidmvlelem5  46614  ovnhoilem1  46616  ovolval5lem1  46667  pimrecltneg  46739  mod42tp1mod8  47589  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrxsphere  48669  itscnhlinecirc02p  48706  iooii  48815  io1ii  48818  sepfsepc  48825  seppcld  48827