Theorem 0xr 11181

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 11178	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11136	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3934	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2109  ℝcr 11027  0cc0 11028  ℝ^*cxr 11167

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 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101

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 3440  df-un 3910  df-ss 3922  df-xr 11172

This theorem is referenced by:  0lepnf  13053  ge0gtmnf  13092  max0sub  13116  xlt0neg1  13139  xlt0neg2  13140  xle0neg1  13141  xle0neg2  13142  xaddf  13144  xaddrid  13161  xaddlid  13162  xnn0xadd0  13167  xaddge0  13178  xsubge0  13181  xposdif  13182  xmullem  13184  xmullem2  13185  xmul01  13187  xmul02  13188  xmulneg1  13189  xmulf  13192  xmulpnf1  13194  xmulasslem2  13202  xmulge0  13204  xmulasslem  13205  xlemul1a  13208  xadddi  13215  xadddi2  13217  dfrp2  13315  ioopos  13345  ioorebas  13372  xrge0neqmnf  13373  elxrge0  13378  0e0iccpnf  13380  xov1plusxeqvd  13419  xnn0xrge0  13427  ico01fl0  13741  rpsup  13788  addmodid  13844  hashgt0  14313  hashle00  14325  hashgt0elex  14326  hashgt23el  14349  sgn0  15014  sgnp  15015  sgnn  15019  fprodge0  15918  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  cos1bnd  16114  sinltx  16116  sin01gt0  16117  cos01gt0  16118  sin02gt0  16119  sincos1sgn  16120  sincos2sgn  16121  halfleoddlt  16291  xrsmgm  21331  leordtval2  23115  pnfnei  23123  mnfnei  23124  psmetge0  24216  isxmet2d  24231  xmetge0  24248  xmetgt0  24262  prdsdsf  24271  prdsxmetlem  24272  xpsdsval  24285  blgt0  24303  xblss2ps  24305  xblss2  24306  xbln0  24318  prdsbl  24395  stdbdxmet  24419  stdbdmopn  24422  metustto  24457  metustid  24458  metustexhalf  24460  cfilucfil  24463  blval2  24466  metuel2  24469  nmoge0  24625  nmo0  24639  cnblcld  24678  blssioo  24699  blcvx  24702  xrsxmet  24714  metdsf  24753  metds0  24755  metdseq0  24759  metnrmlem1a  24763  iccpnfcnv  24858  iccpnfhmeo  24859  xrhmeo  24860  pcoass  24940  iscfil2  25182  ovolmge0  25394  ovolge0  25398  ovolf  25399  ovolssnul  25404  ovolctb  25407  ovoliunnul  25424  ovolicopnf  25441  voliunlem3  25469  volsup  25473  ioorf  25490  volivth  25524  vitalilem4  25528  vitalilem5  25529  itg2ge0  25652  itg2const2  25658  itg2seq  25659  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2gt0  25677  dvne0  25932  mdegle0  25998  ply1remlem  26086  ply1rem  26087  idomrootle  26094  plypf1  26133  aaliou3lem2  26267  aaliou3lem3  26268  taylfvallem1  26280  taylfval  26282  tayl0  26285  radcnvcl  26342  radcnvle  26345  pserulm  26347  psercnlem1  26351  pilem2  26378  sinhalfpilem  26388  sincosq1lem  26422  sincosq1sgn  26423  sincosq2sgn  26424  tangtx  26430  tanabsge  26431  sinq12gt0  26432  cosq14gt0  26435  sincos4thpi  26438  pige3ALT  26445  cos02pilt1  26451  cosq34lt1  26452  cosordlem  26455  cos0pilt1  26457  tanord1  26462  tanord  26463  efifo  26472  argimgt0  26537  argimlt0  26538  logccv  26588  loglesqrt  26687  atantan  26849  rlimcnp  26891  rlimcnp2  26892  scvxcvx  26912  basellem1  27007  dchrisum0lem2a  27444  pntibndlem1  27516  pntibnd  27520  pntlemc  27522  pntlem3  27536  abvcxp  27542  padicabvf  27558  padicabvcxp  27559  ostth2  27564  ttgcontlem1  28848  elntg2  28948  nmooge0  30729  nmoo0  30753  nmlnogt0  30759  nmopge0  31873  nmopgt0  31874  nmfnge0  31889  nmop0  31948  nmfn0  31949  xraddge02  32713  xlt2addrd  32715  xrge0infss  32716  sgncl  32789  sgn3da  32792  elxrge02  32885  xrs0  32973  xrge00  32981  xrge0addass  32983  xrge0addgt0  32984  xrge0adddir  32985  fsumrp0cl  32988  ply1unit  33520  rtelextdg2lem  33692  metider  33860  unitssxrge0  33866  xrge0iifcnv  33899  xrge0iifcv  33900  xrge0iifiso  33901  xrge0iifhom  33903  xrge0mulc1cn  33907  pnfneige0  33917  lmxrge0  33918  esumgsum  34011  esumnul  34014  esum0  34015  esumle  34024  esumlef  34028  esumcst  34029  esumsnf  34030  esumpr2  34033  esumpinfval  34039  esumpinfsum  34043  esumpcvgval  34044  esumpmono  34045  hashf2  34050  esumcvg  34052  measle0  34174  voliune  34195  volfiniune  34196  ddemeas  34202  aean  34210  oms0  34264  prob01  34380  probmeasb  34397  dstfrvclim1  34445  signsply0  34518  chtvalz  34596  hgt750lemf  34620  cvmliftlem10  35266  cvmliftlem13  35268  sinccvglem  35644  dnizeq0  36448  iccioo01  37300  sin2h  37589  tan2h  37591  broucube  37633  mblfinlem2  37637  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  mbfposadd  37646  itg2addnclem2  37651  itg2gt0cn  37654  ftc1anclem5  37676  ftc1anclem8  37679  dvasin  37683  areacirc  37692  rrnequiv  37814  dvrelog2b  42039  aks6d1c5lem3  42110  aks6d1c6lem1  42143  acos1half  42331  redvmptabs  42333  readvrec2  42334  readvrec  42335  imo72b2  44145  absfico  45196  xadd0ge  45301  xrge0nemnfd  45312  xralrple2  45334  xrpnf  45465  pnfel0pnf  45510  ge0xrre  45513  sqrlearg  45535  fsumge0cl  45555  limsup10ex  45755  liminf10ex  45756  sinaover2ne0  45850  itgsin0pilem1  45932  iblsplit  45948  stoweidlem46  46028  fourierdlem43  46132  fourierdlem44  46133  fourierdlem60  46148  fourierdlem61  46149  fourierdlem87  46175  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  etransclem23  46239  salexct2  46321  fge0npnf  46349  fge0iccico  46352  gsumge0cl  46353  sge0z  46357  sge00  46358  sge0sn  46361  sge0tsms  46362  sge0cl  46363  sge0f1o  46364  sge0ge0  46366  sge0repnf  46368  sge0fsum  46369  sge0pr  46376  sge0ssre  46379  sge0prle  46383  sge0p1  46396  sge0iunmptlemre  46397  sge0rpcpnf  46403  sge0rernmpt  46404  sge0isum  46409  sge0ad2en  46413  sge0xaddlem2  46416  sge0uzfsumgt  46426  sge0seq  46428  sge0reuz  46429  voliunsge0lem  46454  meage0  46457  meassre  46459  meale0eq0  46460  meaiuninclem  46462  omessre  46492  omeiunltfirp  46501  carageniuncllem2  46504  carageniuncl  46505  omege0  46515  omess0  46516  hoiprodcl  46529  ovnlerp  46544  ovnf  46545  ovn0lem  46547  ovnsubaddlem1  46552  hoiprodcl3  46562  hoidmvcl  46564  hoidmv1lelem3  46575  hoidmvlelem5  46581  ovnhoilem1  46583  ovolval5lem1  46634  pimrecltneg  46706  rehalfge1  47320  mod42tp1mod8  47587  eenglngeehlnmlem1  48710  eenglngeehlnmlem2  48711  rrxsphere  48721  itscnhlinecirc02p  48758  iooii  48890  io1ii  48893  sepfsepc  48900  seppcld  48902