Theorem 0xr 11228

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 11225	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11183	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3946	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2109  ℝcr 11074  0cc0 11075  ℝ^*cxr 11214

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 2702  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219

This theorem is referenced by:  0lepnf  13100  ge0gtmnf  13139  max0sub  13163  xlt0neg1  13186  xlt0neg2  13187  xle0neg1  13188  xle0neg2  13189  xaddf  13191  xaddrid  13208  xaddlid  13209  xnn0xadd0  13214  xaddge0  13225  xsubge0  13228  xposdif  13229  xmullem  13231  xmullem2  13232  xmul01  13234  xmul02  13235  xmulneg1  13236  xmulf  13239  xmulpnf1  13241  xmulasslem2  13249  xmulge0  13251  xmulasslem  13252  xlemul1a  13255  xadddi  13262  xadddi2  13264  dfrp2  13362  ioopos  13392  ioorebas  13419  xrge0neqmnf  13420  elxrge0  13425  0e0iccpnf  13427  xov1plusxeqvd  13466  xnn0xrge0  13474  ico01fl0  13788  rpsup  13835  addmodid  13891  hashgt0  14360  hashle00  14372  hashgt0elex  14373  hashgt23el  14396  sgn0  15062  sgnp  15063  sgnn  15067  fprodge0  15966  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  cos1bnd  16162  sinltx  16164  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  sincos1sgn  16168  sincos2sgn  16169  halfleoddlt  16339  xrsmgm  21325  leordtval2  23106  pnfnei  23114  mnfnei  23115  psmetge0  24207  isxmet2d  24222  xmetge0  24239  xmetgt0  24253  prdsdsf  24262  prdsxmetlem  24263  xpsdsval  24276  blgt0  24294  xblss2ps  24296  xblss2  24297  xbln0  24309  prdsbl  24386  stdbdxmet  24410  stdbdmopn  24413  metustto  24448  metustid  24449  metustexhalf  24451  cfilucfil  24454  blval2  24457  metuel2  24460  nmoge0  24616  nmo0  24630  cnblcld  24669  blssioo  24690  blcvx  24693  xrsxmet  24705  metdsf  24744  metds0  24746  metdseq0  24750  metnrmlem1a  24754  iccpnfcnv  24849  iccpnfhmeo  24850  xrhmeo  24851  pcoass  24931  iscfil2  25173  ovolmge0  25385  ovolge0  25389  ovolf  25390  ovolssnul  25395  ovolctb  25398  ovoliunnul  25415  ovolicopnf  25432  voliunlem3  25460  volsup  25464  ioorf  25481  volivth  25515  vitalilem4  25519  vitalilem5  25520  itg2ge0  25643  itg2const2  25649  itg2seq  25650  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2gt0  25668  dvne0  25923  mdegle0  25989  ply1remlem  26077  ply1rem  26078  idomrootle  26085  plypf1  26124  aaliou3lem2  26258  aaliou3lem3  26259  taylfvallem1  26271  taylfval  26273  tayl0  26276  radcnvcl  26333  radcnvle  26336  pserulm  26338  psercnlem1  26342  pilem2  26369  sinhalfpilem  26379  sincosq1lem  26413  sincosq1sgn  26414  sincosq2sgn  26415  tangtx  26421  tanabsge  26422  sinq12gt0  26423  cosq14gt0  26426  sincos4thpi  26429  pige3ALT  26436  cos02pilt1  26442  cosq34lt1  26443  cosordlem  26446  cos0pilt1  26448  tanord1  26453  tanord  26454  efifo  26463  argimgt0  26528  argimlt0  26529  logccv  26579  loglesqrt  26678  atantan  26840  rlimcnp  26882  rlimcnp2  26883  scvxcvx  26903  basellem1  26998  dchrisum0lem2a  27435  pntibndlem1  27507  pntibnd  27511  pntlemc  27513  pntlem3  27527  abvcxp  27533  padicabvf  27549  padicabvcxp  27550  ostth2  27555  ttgcontlem1  28819  elntg2  28919  nmooge0  30703  nmoo0  30727  nmlnogt0  30733  nmopge0  31847  nmopgt0  31848  nmfnge0  31863  nmop0  31922  nmfn0  31923  xraddge02  32687  xlt2addrd  32689  xrge0infss  32690  sgncl  32763  sgn3da  32766  elxrge02  32859  xrs0  32951  xrge00  32960  xrge0addass  32964  xrge0addgt0  32965  xrge0adddir  32966  fsumrp0cl  32969  ply1unit  33551  rtelextdg2lem  33723  metider  33891  unitssxrge0  33897  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  xrge0mulc1cn  33938  pnfneige0  33948  lmxrge0  33949  esumgsum  34042  esumnul  34045  esum0  34046  esumle  34055  esumlef  34059  esumcst  34060  esumsnf  34061  esumpr2  34064  esumpinfval  34070  esumpinfsum  34074  esumpcvgval  34075  esumpmono  34076  hashf2  34081  esumcvg  34083  measle0  34205  voliune  34226  volfiniune  34227  ddemeas  34233  aean  34241  oms0  34295  prob01  34411  probmeasb  34428  dstfrvclim1  34476  signsply0  34549  chtvalz  34627  hgt750lemf  34651  cvmliftlem10  35288  cvmliftlem13  35290  sinccvglem  35666  dnizeq0  36470  iccioo01  37322  sin2h  37611  tan2h  37613  broucube  37655  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfposadd  37668  itg2addnclem2  37673  itg2gt0cn  37676  ftc1anclem5  37698  ftc1anclem8  37701  dvasin  37705  areacirc  37714  rrnequiv  37836  dvrelog2b  42061  aks6d1c5lem3  42132  aks6d1c6lem1  42165  acos1half  42353  redvmptabs  42355  readvrec2  42356  readvrec  42357  imo72b2  44168  absfico  45219  xadd0ge  45324  xrge0nemnfd  45335  xralrple2  45357  xrpnf  45488  pnfel0pnf  45533  ge0xrre  45536  sqrlearg  45558  fsumge0cl  45578  limsup10ex  45778  liminf10ex  45779  sinaover2ne0  45873  itgsin0pilem1  45955  iblsplit  45971  stoweidlem46  46051  fourierdlem43  46155  fourierdlem44  46156  fourierdlem60  46171  fourierdlem61  46172  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem23  46262  salexct2  46344  fge0npnf  46372  fge0iccico  46375  gsumge0cl  46376  sge0z  46380  sge00  46381  sge0sn  46384  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0ge0  46389  sge0repnf  46391  sge0fsum  46392  sge0pr  46399  sge0ssre  46402  sge0prle  46406  sge0p1  46419  sge0iunmptlemre  46420  sge0rpcpnf  46426  sge0rernmpt  46427  sge0isum  46432  sge0ad2en  46436  sge0xaddlem2  46439  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  voliunsge0lem  46477  meage0  46480  meassre  46482  meale0eq0  46483  meaiuninclem  46485  omessre  46515  omeiunltfirp  46524  carageniuncllem2  46527  carageniuncl  46528  omege0  46538  omess0  46539  hoiprodcl  46552  ovnlerp  46567  ovnf  46568  ovn0lem  46570  ovnsubaddlem1  46575  hoiprodcl3  46585  hoidmvcl  46587  hoidmv1lelem3  46598  hoidmvlelem5  46604  ovnhoilem1  46606  ovolval5lem1  46657  pimrecltneg  46729  rehalfge1  47340  mod42tp1mod8  47607  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrxsphere  48741  itscnhlinecirc02p  48778  iooii  48910  io1ii  48913  sepfsepc  48920  seppcld  48922