Theorem 0xr 9640

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 9637	. 2 |- RR C_ RR*
2		0re 9596	. 2 |- 0 e. RR
3	1, 2	sselii 3501	1 |- 0 e. RR*

Syntax hints:   e. wcel 1767   RRcr 9491   0cc0 9492   RR*cxr 9627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-i2m1 9560  ax-1ne0 9561  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287  df-xr 9632

This theorem is referenced by:  0lepnf  11340  ge0gtmnf  11373  max0sub  11395  xlt0neg1  11418  xlt0neg2  11419  xle0neg1  11420  xle0neg2  11421  xaddf  11423  xaddid1  11438  xaddid2  11439  xaddge0  11450  xsubge0  11453  xposdif  11454  xmullem  11456  xmullem2  11457  xmul01  11459  xmul02  11460  xmulneg1  11461  xmulf  11464  xmulpnf1  11466  xmulasslem2  11474  xmulge0  11476  xmulasslem  11477  xlemul1a  11480  xadddi  11487  xadddi2  11489  ioopos  11601  ioorebas  11626  elxrge0  11629  0e0iccpnf  11631  xov1plusxeqvd  11666  rpsup  11961  hashgt0  12424  hashle00  12431  hashgt0elex  12432  sgn0  12885  sgnp  12886  sgnn  12890  ef01bndlem  13780  sin01bnd  13781  cos01bnd  13782  cos1bnd  13783  sinltx  13785  sin01gt0  13786  cos01gt0  13787  sin02gt0  13788  sincos1sgn  13789  sincos2sgn  13790  leordtval2  19507  pnfnei  19515  mnfnei  19516  psmetge0  20579  isxmet2d  20593  xmetge0  20610  xmetgt0  20624  prdsdsf  20633  prdsxmetlem  20634  xpsdsval  20647  blgt0  20665  xblss2ps  20667  xblss2  20668  xbln0  20680  prdsbl  20757  stdbdxmet  20781  stdbdmopn  20784  metusttoOLD  20823  metustto  20824  metustidOLD  20825  metustid  20826  metustexhalfOLD  20829  metustexhalf  20830  cfilucfilOLD  20835  cfilucfil  20836  blval2  20841  metuel2  20845  nmoge0  20991  nmo0  21005  cnblcld  21045  blssioo  21063  blcvx  21066  xrsxmet  21077  metdsf  21115  metds0  21117  metdseq0  21121  metnrmlem1a  21125  iccpnfcnv  21207  iccpnfhmeo  21208  xrhmeo  21209  pcoass  21287  iscfil2  21468  ovolmge0  21651  ovolge0  21655  ovolf  21656  ovolssnul  21661  ovolctb  21664  ovoliunnul  21681  ovolicopnf  21698  voliunlem3  21725  volsup  21729  ioorf  21745  volivth  21779  vitalilem4  21783  vitalilem5  21784  itg2ge0  21905  itg2const2  21911  itg2seq  21912  itg2monolem1  21920  itg2monolem2  21921  itg2monolem3  21922  itg2gt0  21930  dvne0  22175  mdegle0  22240  ply1remlem  22326  ply1rem  22327  plypf1  22372  aaliou3lem2  22501  aaliou3lem3  22502  taylfvallem1  22514  taylfval  22516  tayl0  22519  radcnvcl  22574  radcnvle  22577  pserulm  22579  psercnlem1  22582  pilem2  22609  sinhalfpilem  22617  sincosq1lem  22651  sincosq1sgn  22652  sincosq2sgn  22653  tangtx  22659  tanabsge  22660  sinq12gt0  22661  cosq14gt0  22664  sincos4thpi  22667  pige3  22671  cosordlem  22679  tanord1  22685  tanord  22686  efifo  22695  argimgt0  22753  argimlt0  22754  logccv  22800  loglesqrt  22888  atantan  23010  rlimcnp  23051  rlimcnp2  23052  scvxcvx  23071  basellem1  23110  dchrisum0lem2a  23458  pntibndlem1  23530  pntibnd  23534  pntlemc  23536  pntlem3  23550  abvcxp  23556  padicabvf  23572  padicabvcxp  23573  ostth2  23578  ttgcontlem1  23892  nmooge0  25386  nmoo0  25410  nmlnogt0  25416  nmopge0  26534  nmopgt0  26535  nmfnge0  26550  nmop0  26609  nmfn0  26610  xraddge02  27273  xlt2addrd  27274  xrge0infss  27276  elxrge02  27324  xrs0  27353  xrge00  27364  xrge0addass  27368  xrge0neqmnf  27369  xrge0addgt0  27371  xrge0adddir  27372  fsumrp0cl  27375  metider  27537  unitssxrge0  27546  xrge0iifcnv  27579  xrge0iifcv  27580  xrge0iifiso  27581  xrge0iifhom  27583  xrge0mulc1cn  27587  pnfneige0  27597  lmxrge0  27598  esumnul  27727  esum0  27728  esumle  27733  esumlef  27738  esumcst  27739  esumsn  27740  esumpr2  27742  esumpinfval  27747  esumpinfsum  27751  esumpcvgval  27752  esumpmono  27753  hashf2  27758  esumcvg  27760  measle0  27847  voliune  27869  volfiniune  27870  ddemeas  27876  aean  27884  oms0  27934  prob01  28020  probmeasb  28037  dstfrvclim1  28084  sgncl  28145  sgn3da  28148  sgn0bi  28154  cvmliftlem10  28407  cvmliftlem13  28409  sinccvglem  28541  sin2h  29650  tan2h  29652  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  volsupnfl  29664  mbfposadd  29667  itg2addnclem2  29672  itg2gt0cn  29675  ftc1anclem5  29699  ftc1anclem8  29702  dvasin  29708  areacirc  29717  rrnequiv  29962  idomrootle  30785  sinaover2ne0  31232  itgsin0pilem1  31295  iblsplit  31312  stoweidlem46  31374  fourierdlem43  31478  fourierdlem44  31479  fourierdlem60  31495  fourierdlem61  31496  fourierdlem87  31522  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560  bj-flbi3  33697