Theorem 0xr 9705

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 9702	. 2 |- RR C_ RR*
2		0re 9661	. 2 |- 0 e. RR
3	1, 2	sselii 3415	1 |- 0 e. RR*

Syntax hints:   e. wcel 1904   RRcr 9556   0cc0 9557   RR*cxr 9692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-i2m1 9625  ax-1ne0 9626  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597  df-ov 6311  df-xr 9697

This theorem is referenced by:  0lepnf  11456  ge0gtmnf  11490  max0sub  11512  xlt0neg1  11535  xlt0neg2  11536  xle0neg1  11537  xle0neg2  11538  xaddf  11540  xaddid1  11556  xaddid2  11557  xaddge0  11569  xsubge0  11572  xposdif  11573  xmullem  11575  xmullem2  11576  xmul01  11578  xmul02  11579  xmulneg1  11580  xmulf  11583  xmulpnf1  11585  xmulasslem2  11593  xmulge0  11595  xmulasslem  11596  xlemul1a  11599  xadddi  11606  xadddi2  11608  ioopos  11736  ioorebas  11761  xrge0neqmnf  11762  elxrge0  11767  0e0iccpnf  11769  xov1plusxeqvd  11804  ico01fl0  12086  rpsup  12126  addmodid  12172  hashgt0  12605  hashle00  12615  hashgt0elex  12616  sgn0  13229  sgnp  13230  sgnn  13234  fprodge0  14124  ef01bndlem  14315  sin01bnd  14316  cos01bnd  14317  cos1bnd  14318  sinltx  14320  sin01gt0  14321  cos01gt0  14322  sin02gt0  14323  sincos1sgn  14324  sincos2sgn  14325  xrsmgm  19080  leordtval2  20305  pnfnei  20313  mnfnei  20314  psmetge0  21406  isxmet2d  21420  xmetge0  21437  xmetgt0  21451  prdsdsf  21460  prdsxmetlem  21461  xpsdsval  21474  blgt0  21492  xblss2ps  21494  xblss2  21495  xbln0  21507  prdsbl  21584  stdbdxmet  21608  stdbdmopn  21611  metustto  21646  metustid  21647  metustexhalf  21649  cfilucfil  21652  blval2  21655  metuel2  21658  nmoge0  21804  nmoge0OLD  21822  nmo0  21834  cnblcld  21873  blssioo  21891  blcvx  21894  xrsxmet  21905  metdsf  21943  metds0  21945  metdseq0  21949  metnrmlem1a  21953  metdsfOLD  21958  metds0OLD  21960  metdseq0OLD  21964  metnrmlem1aOLD  21968  iccpnfcnv  22050  iccpnfhmeo  22051  xrhmeo  22052  pcoass  22133  iscfil2  22314  ovolmge0  22508  ovolge0  22512  ovolf  22513  ovolssnul  22518  ovolctb  22521  ovoliunnul  22538  ovolicopnf  22556  voliunlem3  22584  volsup  22588  ioorf  22604  ioorfOLD  22609  volivth  22644  vitalilem4  22648  vitalilem5  22649  itg2ge0  22772  itg2const2  22778  itg2seq  22779  itg2monolem1  22787  itg2monolem2  22788  itg2monolem3  22789  itg2gt0  22797  dvne0  23042  mdegle0  23105  ply1remlem  23192  ply1rem  23193  plypf1  23245  aaliou3lem2  23378  aaliou3lem3  23379  taylfvallem1  23391  taylfval  23393  tayl0  23396  radcnvcl  23451  radcnvle  23454  pserulm  23456  psercnlem1  23459  pilem2  23486  pilem2OLD  23487  sinhalfpilem  23497  sincosq1lem  23531  sincosq1sgn  23532  sincosq2sgn  23533  tangtx  23539  tanabsge  23540  sinq12gt0  23541  cosq14gt0  23544  sincos4thpi  23547  pige3  23551  cosordlem  23559  tanord1  23565  tanord  23566  efifo  23575  argimgt0  23640  argimlt0  23641  logccv  23687  loglesqrt  23777  atantan  23928  rlimcnp  23970  rlimcnp2  23971  scvxcvx  23990  basellem1  24086  dchrisum0lem2a  24434  pntibndlem1  24506  pntibnd  24510  pntlemc  24512  pntlem3  24526  abvcxp  24532  padicabvf  24548  padicabvcxp  24549  ostth2  24554  ttgcontlem1  24994  nmooge0  26489  nmoo0  26513  nmlnogt0  26519  nmopge0  27645  nmopgt0  27646  nmfnge0  27661  nmop0  27720  nmfn0  27721  xraddge02  28411  xlt2addrd  28413  xrge0infss  28415  xrge0infssOLD  28416  dfrp2  28427  elxrge02  28476  xrs0  28512  xrge00  28523  xrge0addass  28527  xrge0addgt0  28528  xrge0adddir  28529  fsumrp0cl  28532  metider  28771  unitssxrge0  28780  xrge0iifcnv  28813  xrge0iifcv  28814  xrge0iifiso  28815  xrge0iifhom  28817  xrge0mulc1cn  28821  pnfneige0  28831  lmxrge0  28832  esumgsum  28940  esumnul  28943  esum0  28944  esumle  28953  esumlef  28957  esumcst  28958  esumsnf  28959  esumpr2  28962  esumpinfval  28968  esumpinfsum  28972  esumpcvgval  28973  esumpmono  28974  hashf2  28979  esumcvg  28981  measle0  29104  voliune  29125  volfiniune  29126  ddemeas  29132  aean  29140  oms0  29198  oms0OLD  29202  prob01  29319  probmeasb  29336  dstfrvclim1  29383  sgncl  29482  sgn3da  29485  signsply0  29512  cvmliftlem10  30089  cvmliftlem13  30091  sinccvglem  30388  sin2h  31999  tan2h  32001  broucube  32038  mblfinlem2  32042  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  mbfposadd  32052  itg2addnclem2  32058  itg2gt0cn  32061  ftc1anclem5  32085  ftc1anclem8  32088  dvasin  32092  areacirc  32101  rrnequiv  32231  idomrootle  36140  imo72b2  36689  absfico  37571  xadd0ge  37630  xrge0nemnfd  37642  xralrple2  37664  pnfel0pnf  37725  ge0nemnf2  37726  ge0xrre  37729  fsumge0cl  37748  sinaover2ne0  37840  itgsin0pilem1  37923  iblsplit  37940  stoweidlem46  38019  fourierdlem43  38126  fourierdlem44  38127  fourierdlem60  38142  fourierdlem61  38143  fourierdlem87  38169  fourierdlem103  38185  fourierdlem104  38186  fourierdlem111  38193  sqwvfourb  38205  fourierswlem  38206  fouriersw  38207  etransclem23  38234  salexct2  38310  fge0npnf  38323  fge0iccico  38326  gsumge0cl  38327  sge0z  38331  sge00  38332  sge0sn  38335  sge0tsms  38336  sge0cl  38337  sge0f1o  38338  sge0ge0  38340  sge0repnf  38342  sge0fsum  38343  sge0pr  38350  sge0ssre  38353  sge0prle  38357  sge0p1  38370  sge0iunmptlemre  38371  sge0rpcpnf  38377  sge0rernmpt  38378  sge0isum  38383  sge0ad2en  38387  sge0xaddlem2  38390  sge0uzfsumgt  38400  sge0seq  38402  voliunsge0lem  38426  omessre  38450  omeiunltfirp  38459  carageniuncllem2  38462  carageniuncl  38463  omege0  38473  omess0  38474  hoiprodcl  38487  ovnlerp  38502  ovnf  38503  ovn0lem  38505  ovnsubaddlem1  38510  hoiprodcl3  38520  hoidmvcl  38522  hoidmv1lelem3  38533  hoidmvlelem5  38539  ovnhoilem1  38541  ovolval5lem1  38592  xnn0xrge0  39226  xnn0xadd0  39238