Theorem 0xr 9087

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	|- 0 e. RR*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 9085	. 2 |- RR C_ RR*
2		0re 9047	. 2 |- 0 e. RR
3	1, 2	sselii 3305	1 |- 0 e. RR*

Syntax hints:   e. wcel 1721   RRcr 8945   0cc0 8946   RR*cxr 9075

This theorem is referenced by:  nn0pnfge0  10684  ge0gtmnf  10716  max0sub  10738  xlt0neg1  10761  xlt0neg2  10762  xle0neg1  10763  xle0neg2  10764  xaddf  10766  xaddid1  10781  xaddid2  10782  xaddge0  10793  xsubge0  10796  xposdif  10797  xmullem  10799  xmullem2  10800  xmul01  10802  xmul02  10803  xmulneg1  10804  xmulf  10807  xmulpnf1  10809  xmulasslem2  10817  xmulge0  10819  xmulasslem  10820  xlemul1a  10823  xadddi  10830  xadddi2  10832  ioopos  10943  ioorebas  10962  elxrge0  10964  xov1plusxeqvd  10997  rpsup  11202  hashgt0  11617  hashle00  11624  hashgt0elex  11625  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos1bnd  12743  sinltx  12745  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  sincos1sgn  12749  sincos2sgn  12750  pcge0  13190  xrge0subm  16694  leordtval2  17230  pnfnei  17238  mnfnei  17239  psmetge0  18296  isxmet2d  18310  xmetge0  18327  xmetgt0  18341  prdsdsf  18350  prdsxmetlem  18351  xpsdsval  18364  blgt0  18382  xblss2ps  18384  xblss2  18385  xbln0  18397  prdsbl  18474  stdbdxmet  18498  stdbdmopn  18501  metusttoOLD  18540  metustto  18541  metustidOLD  18542  metustid  18543  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  blval2  18558  metuel2  18562  nmoge0  18708  nmo0  18722  cnblcld  18762  blssioo  18779  blcvx  18782  xrsxmet  18793  metdsf  18831  metds0  18833  metdseq0  18837  metnrmlem1a  18841  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  pcoass  19002  iscfil2  19172  ovolmge0  19326  ovolge0  19330  ovolf  19331  ovolssnul  19336  ovolctb  19339  ovoliunnul  19356  ovolicopnf  19373  voliunlem3  19399  volsup  19403  ioorf  19418  volivth  19452  vitalilem4  19456  vitalilem5  19457  itg2ge0  19580  itg2const2  19586  itg2seq  19587  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2gt0  19605  itg2cnlem2  19607  itg2cn  19608  iblss  19649  itgle  19654  itgeqa  19658  ibladdlem  19664  iblabs  19673  iblabsr  19674  iblmulc2  19675  bddmulibl  19683  dvne0  19848  mdegle0  19953  ply1remlem  20038  ply1rem  20039  plypf1  20084  aaliou3lem2  20213  aaliou3lem3  20214  taylfvallem1  20226  taylfval  20228  tayl0  20231  radcnvcl  20286  radcnvle  20289  pserulm  20291  psercnlem1  20294  pilem2  20321  sinhalfpilem  20327  sincosq1lem  20358  sincosq1sgn  20359  sincosq2sgn  20360  tangtx  20366  tanabsge  20367  sinq12gt0  20368  cosq14gt0  20371  sincos4thpi  20374  pige3  20378  cosordlem  20386  tanord1  20392  tanord  20393  efifo  20402  argimgt0  20460  argimlt0  20461  logccv  20507  loglesqr  20595  atantan  20716  rlimcnp  20757  rlimcnp2  20758  rlimcnp3  20759  scvxcvx  20777  basellem1  20816  dchrisum0lem2a  21164  pntibndlem1  21236  pntibnd  21240  pntlemc  21242  pntlem3  21256  abvcxp  21262  padicabvf  21278  padicabvcxp  21279  ostth2  21284  nmooge0  22221  nmoo0  22245  nmlnogt0  22251  nmopge0  23367  nmopgt0  23368  nmfnge0  23383  nmop0  23442  nmfn0  23443  xraddge02  24076  xlt2addrd  24077  elxrge02  24131  xrs0  24150  xrge00  24161  xrge0addass  24164  xrge0neqmnf  24165  xrge0addgt0  24167  xrge0adddir  24168  fsumrp0cl  24170  metider  24242  unitssxrge0  24251  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhom  24276  xrge0mulc1cn  24280  pnfneige0  24289  lmxrge0  24290  esumnul  24396  esum0  24397  esumle  24402  esumlef  24407  esumcst  24408  esumsn  24409  esumpr2  24411  esumpinfval  24416  esumpfinvallem  24417  esumpinfsum  24420  esumpcvgval  24421  esumpmono  24422  esummulc1  24424  hashf2  24427  esumcvg  24429  measle0  24515  voliune  24538  volfiniune  24539  aean  24548  prob01  24624  probmeasb  24641  dstfrvclim1  24688  cvmliftlem10  24934  cvmliftlem13  24936  sinccvglem  25062  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfposadd  26153  itg2addnclem2  26156  itg2gt0cn  26159  ibladdnclem  26160  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  dvreasin  26179  areacirc  26187  rrnequiv  26434  idomrootle  27379  itgsin0pilem1  27611  stoweidlem46  27662  sgn0  28233  sgnp  28234  sgnn  28238

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-xr 9080