Theorem 0xr 11305

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 11302	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11260	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3991	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2105  ℝcr 11151  0cc0 11152  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296

This theorem is referenced by:  0lepnf  13171  ge0gtmnf  13210  max0sub  13234  xlt0neg1  13257  xlt0neg2  13258  xle0neg1  13259  xle0neg2  13260  xaddf  13262  xaddrid  13279  xaddlid  13280  xnn0xadd0  13285  xaddge0  13296  xsubge0  13299  xposdif  13300  xmullem  13302  xmullem2  13303  xmul01  13305  xmul02  13306  xmulneg1  13307  xmulf  13310  xmulpnf1  13312  xmulasslem2  13320  xmulge0  13322  xmulasslem  13323  xlemul1a  13326  xadddi  13333  xadddi2  13335  dfrp2  13432  ioopos  13460  ioorebas  13487  xrge0neqmnf  13488  elxrge0  13493  0e0iccpnf  13495  xov1plusxeqvd  13534  xnn0xrge0  13542  ico01fl0  13855  rpsup  13902  addmodid  13956  hashgt0  14423  hashle00  14435  hashgt0elex  14436  hashgt23el  14459  sgn0  15124  sgnp  15125  sgnn  15129  fprodge0  16025  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  sinltx  16221  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  sincos1sgn  16225  sincos2sgn  16226  halfleoddlt  16395  xrsmgm  21436  leordtval2  23235  pnfnei  23243  mnfnei  23244  psmetge0  24337  isxmet2d  24352  xmetge0  24369  xmetgt0  24383  prdsdsf  24392  prdsxmetlem  24393  xpsdsval  24406  blgt0  24424  xblss2ps  24426  xblss2  24427  xbln0  24439  prdsbl  24519  stdbdxmet  24543  stdbdmopn  24546  metustto  24581  metustid  24582  metustexhalf  24584  cfilucfil  24587  blval2  24590  metuel2  24593  nmoge0  24757  nmo0  24771  cnblcld  24810  blssioo  24830  blcvx  24833  xrsxmet  24844  metdsf  24883  metds0  24885  metdseq0  24889  metnrmlem1a  24893  iccpnfcnv  24988  iccpnfhmeo  24989  xrhmeo  24990  pcoass  25070  iscfil2  25313  ovolmge0  25525  ovolge0  25529  ovolf  25530  ovolssnul  25535  ovolctb  25538  ovoliunnul  25555  ovolicopnf  25572  voliunlem3  25600  volsup  25604  ioorf  25621  volivth  25655  vitalilem4  25659  vitalilem5  25660  itg2ge0  25784  itg2const2  25790  itg2seq  25791  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2gt0  25809  dvne0  26064  mdegle0  26130  ply1remlem  26218  ply1rem  26219  idomrootle  26226  plypf1  26265  aaliou3lem2  26399  aaliou3lem3  26400  taylfvallem1  26412  taylfval  26414  tayl0  26417  radcnvcl  26474  radcnvle  26477  pserulm  26479  psercnlem1  26483  pilem2  26510  sinhalfpilem  26519  sincosq1lem  26553  sincosq1sgn  26554  sincosq2sgn  26555  tangtx  26561  tanabsge  26562  sinq12gt0  26563  cosq14gt0  26566  sincos4thpi  26569  pige3ALT  26576  cos02pilt1  26582  cosq34lt1  26583  cosordlem  26586  cos0pilt1  26588  tanord1  26593  tanord  26594  efifo  26603  argimgt0  26668  argimlt0  26669  logccv  26719  loglesqrt  26818  atantan  26980  rlimcnp  27022  rlimcnp2  27023  scvxcvx  27043  basellem1  27138  dchrisum0lem2a  27575  pntibndlem1  27647  pntibnd  27651  pntlemc  27653  pntlem3  27667  abvcxp  27673  padicabvf  27689  padicabvcxp  27690  ostth2  27695  ttgcontlem1  28913  elntg2  29014  nmooge0  30795  nmoo0  30819  nmlnogt0  30825  nmopge0  31939  nmopgt0  31940  nmfnge0  31955  nmop0  32014  nmfn0  32015  xraddge02  32766  xlt2addrd  32768  xrge0infss  32770  elxrge02  32898  xrs0  32990  xrge00  32999  xrge0addass  33003  xrge0addgt0  33004  xrge0adddir  33005  fsumrp0cl  33008  ply1unit  33579  rtelextdg2lem  33731  metider  33854  unitssxrge0  33860  xrge0iifcnv  33893  xrge0iifcv  33894  xrge0iifiso  33895  xrge0iifhom  33897  xrge0mulc1cn  33901  pnfneige0  33911  lmxrge0  33912  esumgsum  34025  esumnul  34028  esum0  34029  esumle  34038  esumlef  34042  esumcst  34043  esumsnf  34044  esumpr2  34047  esumpinfval  34053  esumpinfsum  34057  esumpcvgval  34058  esumpmono  34059  hashf2  34064  esumcvg  34066  measle0  34188  voliune  34209  volfiniune  34210  ddemeas  34216  aean  34224  oms0  34278  prob01  34394  probmeasb  34411  dstfrvclim1  34458  sgncl  34519  sgn3da  34522  signsply0  34544  chtvalz  34622  hgt750lemf  34646  cvmliftlem10  35278  cvmliftlem13  35280  sinccvglem  35656  dnizeq0  36457  iccioo01  37309  sin2h  37596  tan2h  37598  broucube  37640  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfposadd  37653  itg2addnclem2  37658  itg2gt0cn  37661  ftc1anclem5  37683  ftc1anclem8  37686  dvasin  37690  areacirc  37699  rrnequiv  37821  dvrelog2b  42047  aks6d1c5lem3  42118  aks6d1c6lem1  42151  acos1half  42366  redvmptabs  42368  readvrec2  42369  readvrec  42370  imo72b2  44161  absfico  45160  xadd0ge  45270  xrge0nemnfd  45281  xralrple2  45303  xrpnf  45435  pnfel0pnf  45480  ge0xrre  45483  sqrlearg  45505  fsumge0cl  45528  limsup10ex  45728  liminf10ex  45729  sinaover2ne0  45823  itgsin0pilem1  45905  iblsplit  45921  stoweidlem46  46001  fourierdlem43  46105  fourierdlem44  46106  fourierdlem60  46121  fourierdlem61  46122  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem23  46212  salexct2  46294  fge0npnf  46322  fge0iccico  46325  gsumge0cl  46326  sge0z  46330  sge00  46331  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0ge0  46339  sge0repnf  46341  sge0fsum  46342  sge0pr  46349  sge0ssre  46352  sge0prle  46356  sge0p1  46369  sge0iunmptlemre  46370  sge0rpcpnf  46376  sge0rernmpt  46377  sge0isum  46382  sge0ad2en  46386  sge0xaddlem2  46389  sge0uzfsumgt  46399  sge0seq  46401  sge0reuz  46402  voliunsge0lem  46427  meage0  46430  meassre  46432  meale0eq0  46433  meaiuninclem  46435  omessre  46465  omeiunltfirp  46474  carageniuncllem2  46477  carageniuncl  46478  omege0  46488  omess0  46489  hoiprodcl  46502  ovnlerp  46517  ovnf  46518  ovn0lem  46520  ovnsubaddlem1  46525  hoiprodcl3  46535  hoidmvcl  46537  hoidmv1lelem3  46548  hoidmvlelem5  46554  ovnhoilem1  46556  ovolval5lem1  46607  pimrecltneg  46679  mod42tp1mod8  47526  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrxsphere  48597  itscnhlinecirc02p  48634  iooii  48713  io1ii  48716  sepfsepc  48723  seppcld  48725