Theorem 0xr 9643

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 9640	. 2 |- RR C_ RR*
2		0re 9599	. 2 |- 0 e. RR
3	1, 2	sselii 3486	1 |- 0 e. RR*

Syntax hints:   e. wcel 1804   RRcr 9494   0cc0 9495   RR*cxr 9630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-xr 9635

This theorem is referenced by:  0lepnf  11351  ge0gtmnf  11384  max0sub  11406  xlt0neg1  11429  xlt0neg2  11430  xle0neg1  11431  xle0neg2  11432  xaddf  11434  xaddid1  11449  xaddid2  11450  xaddge0  11461  xsubge0  11464  xposdif  11465  xmullem  11467  xmullem2  11468  xmul01  11470  xmul02  11471  xmulneg1  11472  xmulf  11475  xmulpnf1  11477  xmulasslem2  11485  xmulge0  11487  xmulasslem  11488  xlemul1a  11491  xadddi  11498  xadddi2  11500  ioopos  11612  ioorebas  11637  elxrge0  11640  0e0iccpnf  11642  xov1plusxeqvd  11677  rpsup  11975  hashgt0  12438  hashle00  12447  hashgt0elex  12448  sgn0  12904  sgnp  12905  sgnn  12909  ef01bndlem  13901  sin01bnd  13902  cos01bnd  13903  cos1bnd  13904  sinltx  13906  sin01gt0  13907  cos01gt0  13908  sin02gt0  13909  sincos1sgn  13910  sincos2sgn  13911  xrsmgm  18432  leordtval2  19691  pnfnei  19699  mnfnei  19700  psmetge0  20794  isxmet2d  20808  xmetge0  20825  xmetgt0  20839  prdsdsf  20848  prdsxmetlem  20849  xpsdsval  20862  blgt0  20880  xblss2ps  20882  xblss2  20883  xbln0  20895  prdsbl  20972  stdbdxmet  20996  stdbdmopn  20999  metusttoOLD  21038  metustto  21039  metustidOLD  21040  metustid  21041  metustexhalfOLD  21044  metustexhalf  21045  cfilucfilOLD  21050  cfilucfil  21051  blval2  21056  metuel2  21060  nmoge0  21206  nmo0  21220  cnblcld  21260  blssioo  21278  blcvx  21281  xrsxmet  21292  metdsf  21330  metds0  21332  metdseq0  21336  metnrmlem1a  21340  iccpnfcnv  21422  iccpnfhmeo  21423  xrhmeo  21424  pcoass  21502  iscfil2  21683  ovolmge0  21866  ovolge0  21870  ovolf  21871  ovolssnul  21876  ovolctb  21879  ovoliunnul  21896  ovolicopnf  21913  voliunlem3  21940  volsup  21944  ioorf  21960  volivth  21994  vitalilem4  21998  vitalilem5  21999  itg2ge0  22120  itg2const2  22126  itg2seq  22127  itg2monolem1  22135  itg2monolem2  22136  itg2monolem3  22137  itg2gt0  22145  dvne0  22390  mdegle0  22455  ply1remlem  22541  ply1rem  22542  plypf1  22587  aaliou3lem2  22717  aaliou3lem3  22718  taylfvallem1  22730  taylfval  22732  tayl0  22735  radcnvcl  22790  radcnvle  22793  pserulm  22795  psercnlem1  22798  pilem2  22825  sinhalfpilem  22834  sincosq1lem  22868  sincosq1sgn  22869  sincosq2sgn  22870  tangtx  22876  tanabsge  22877  sinq12gt0  22878  cosq14gt0  22881  sincos4thpi  22884  pige3  22888  cosordlem  22896  tanord1  22902  tanord  22903  efifo  22912  argimgt0  22975  argimlt0  22976  logccv  23022  loglesqrt  23110  atantan  23232  rlimcnp  23273  rlimcnp2  23274  scvxcvx  23293  basellem1  23332  dchrisum0lem2a  23680  pntibndlem1  23752  pntibnd  23756  pntlemc  23758  pntlem3  23772  abvcxp  23778  padicabvf  23794  padicabvcxp  23795  ostth2  23800  ttgcontlem1  24166  nmooge0  25660  nmoo0  25684  nmlnogt0  25690  nmopge0  26808  nmopgt0  26809  nmfnge0  26824  nmop0  26883  nmfn0  26884  xraddge02  27555  xlt2addrd  27556  xrge0infss  27558  elxrge02  27606  xrs0  27641  xrge00  27652  xrge0addass  27656  xrge0neqmnf  27657  xrge0addgt0  27659  xrge0adddir  27660  fsumrp0cl  27663  metider  27851  unitssxrge0  27860  xrge0iifcnv  27893  xrge0iifcv  27894  xrge0iifiso  27895  xrge0iifhom  27897  xrge0mulc1cn  27901  pnfneige0  27911  lmxrge0  27912  esumnul  28037  esum0  28038  esumle  28043  esumlef  28048  esumcst  28049  esumsn  28050  esumpr2  28052  esumpinfval  28057  esumpinfsum  28061  esumpcvgval  28062  esumpmono  28063  hashf2  28068  esumcvg  28070  measle0  28157  voliune  28179  volfiniune  28180  ddemeas  28186  aean  28194  oms0  28244  prob01  28330  probmeasb  28347  dstfrvclim1  28394  sgncl  28455  sgn3da  28458  signsply0  28486  cvmliftlem10  28717  cvmliftlem13  28719  sinccvglem  29016  sin2h  30021  tan2h  30023  mblfinlem2  30028  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  mbfposadd  30038  itg2addnclem2  30043  itg2gt0cn  30046  ftc1anclem5  30070  ftc1anclem8  30073  dvasin  30079  areacirc  30088  rrnequiv  30307  idomrootle  31128  fprodge0  31551  sinaover2ne0  31622  itgsin0pilem1  31702  iblsplit  31719  stoweidlem46  31782  fourierdlem43  31886  fourierdlem44  31887  fourierdlem60  31903  fourierdlem61  31904  fourierdlem87  31930  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  sqwvfourb  31966  fourierswlem  31967  fouriersw  31968  etransclem23  31994  bj-flbi3  34483  imo72b2  37797