Theorem 0xr 9692

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 9689	. 2 |- RR C_ RR*
2		0re 9648	. 2 |- 0 e. RR
3	1, 2	sselii 3431	1 |- 0 e. RR*

Syntax hints:   e. wcel 1889   RRcr 9543   0cc0 9544   RR*cxr 9679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-i2m1 9612  ax-1ne0 9613  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-iota 5549  df-fv 5593  df-ov 6298  df-xr 9684

This theorem is referenced by:  0lepnf  11440  ge0gtmnf  11474  max0sub  11496  xlt0neg1  11519  xlt0neg2  11520  xle0neg1  11521  xle0neg2  11522  xaddf  11524  xaddid1  11539  xaddid2  11540  xaddge0  11551  xsubge0  11554  xposdif  11555  xmullem  11557  xmullem2  11558  xmul01  11560  xmul02  11561  xmulneg1  11562  xmulf  11565  xmulpnf1  11567  xmulasslem2  11575  xmulge0  11577  xmulasslem  11578  xlemul1a  11581  xadddi  11588  xadddi2  11590  ioopos  11718  ioorebas  11743  xrge0neqmnf  11744  elxrge0  11748  0e0iccpnf  11750  xov1plusxeqvd  11785  ico01fl0  12060  rpsup  12100  addmodid  12146  hashgt0  12574  hashle00  12584  hashgt0elex  12585  sgn0  13164  sgnp  13165  sgnn  13169  fprodge0  14059  ef01bndlem  14250  sin01bnd  14251  cos01bnd  14252  cos1bnd  14253  sinltx  14255  sin01gt0  14256  cos01gt0  14257  sin02gt0  14258  sincos1sgn  14259  sincos2sgn  14260  xrsmgm  19015  leordtval2  20240  pnfnei  20248  mnfnei  20249  psmetge0  21340  isxmet2d  21354  xmetge0  21371  xmetgt0  21385  prdsdsf  21394  prdsxmetlem  21395  xpsdsval  21408  blgt0  21426  xblss2ps  21428  xblss2  21429  xbln0  21441  prdsbl  21518  stdbdxmet  21542  stdbdmopn  21545  metustto  21580  metustid  21581  metustexhalf  21583  cfilucfil  21586  blval2  21589  metuel2  21592  nmoge0  21738  nmoge0OLD  21756  nmo0  21768  cnblcld  21807  blssioo  21825  blcvx  21828  xrsxmet  21839  metdsf  21877  metds0  21879  metdseq0  21883  metnrmlem1a  21887  metdsfOLD  21892  metds0OLD  21894  metdseq0OLD  21898  metnrmlem1aOLD  21902  iccpnfcnv  21984  iccpnfhmeo  21985  xrhmeo  21986  pcoass  22067  iscfil2  22248  ovolmge0  22442  ovolge0  22446  ovolf  22447  ovolssnul  22452  ovolctb  22455  ovoliunnul  22472  ovolicopnf  22490  voliunlem3  22517  volsup  22521  ioorf  22537  ioorfOLD  22542  volivth  22577  vitalilem4  22581  vitalilem5  22582  itg2ge0  22705  itg2const2  22711  itg2seq  22712  itg2monolem1  22720  itg2monolem2  22721  itg2monolem3  22722  itg2gt0  22730  dvne0  22975  mdegle0  23038  ply1remlem  23125  ply1rem  23126  plypf1  23178  aaliou3lem2  23311  aaliou3lem3  23312  taylfvallem1  23324  taylfval  23326  tayl0  23329  radcnvcl  23384  radcnvle  23387  pserulm  23389  psercnlem1  23392  pilem2  23419  pilem2OLD  23420  sinhalfpilem  23430  sincosq1lem  23464  sincosq1sgn  23465  sincosq2sgn  23466  tangtx  23472  tanabsge  23473  sinq12gt0  23474  cosq14gt0  23477  sincos4thpi  23480  pige3  23484  cosordlem  23492  tanord1  23498  tanord  23499  efifo  23508  argimgt0  23573  argimlt0  23574  logccv  23620  loglesqrt  23710  atantan  23861  rlimcnp  23903  rlimcnp2  23904  scvxcvx  23923  basellem1  24019  dchrisum0lem2a  24367  pntibndlem1  24439  pntibnd  24443  pntlemc  24445  pntlem3  24459  abvcxp  24465  padicabvf  24481  padicabvcxp  24482  ostth2  24487  ttgcontlem1  24927  nmooge0  26420  nmoo0  26444  nmlnogt0  26450  nmopge0  27576  nmopgt0  27577  nmfnge0  27592  nmop0  27651  nmfn0  27652  xraddge02  28348  xlt2addrd  28350  xrge0infss  28352  xrge0infssOLD  28353  dfrp2  28364  elxrge02  28413  xrs0  28449  xrge00  28460  xrge0addass  28464  xrge0addgt0  28466  xrge0adddir  28467  fsumrp0cl  28470  metider  28709  unitssxrge0  28718  xrge0iifcnv  28751  xrge0iifcv  28752  xrge0iifiso  28753  xrge0iifhom  28755  xrge0mulc1cn  28759  pnfneige0  28769  lmxrge0  28770  esumgsum  28878  esumnul  28881  esum0  28882  esumle  28891  esumlef  28895  esumcst  28896  esumsnf  28897  esumpr2  28900  esumpinfval  28906  esumpinfsum  28910  esumpcvgval  28911  esumpmono  28912  hashf2  28917  esumcvg  28919  measle0  29042  voliune  29064  volfiniune  29065  ddemeas  29071  aean  29079  oms0  29137  oms0OLD  29141  prob01  29258  probmeasb  29275  dstfrvclim1  29322  sgncl  29421  sgn3da  29424  signsply0  29452  cvmliftlem10  30029  cvmliftlem13  30031  sinccvglem  30328  sin2h  31947  tan2h  31949  broucube  31986  mblfinlem2  31990  ovoliunnfl  31994  voliunnfl  31996  volsupnfl  31997  mbfposadd  32000  itg2addnclem2  32006  itg2gt0cn  32009  ftc1anclem5  32033  ftc1anclem8  32036  dvasin  32040  areacirc  32049  rrnequiv  32179  idomrootle  36081  imo72b2  36630  xadd0ge  37552  xrge0nemnfd  37565  xralrple2  37587  pnfel0pnf  37639  ge0nemnf2  37640  ge0xrre  37643  fsumge0cl  37662  sinaover2ne0  37753  itgsin0pilem1  37836  iblsplit  37853  stoweidlem46  37917  fourierdlem43  38024  fourierdlem44  38025  fourierdlem60  38040  fourierdlem61  38041  fourierdlem87  38067  fourierdlem103  38083  fourierdlem104  38084  fourierdlem111  38091  sqwvfourb  38103  fourierswlem  38104  fouriersw  38105  etransclem23  38132  salexct2  38208  fge0npnf  38219  fge0iccico  38222  gsumge0cl  38223  sge0z  38227  sge00  38228  sge0sn  38231  sge0tsms  38232  sge0cl  38233  sge0f1o  38234  sge0ge0  38236  sge0repnf  38238  sge0fsum  38239  sge0pr  38246  sge0ssre  38249  sge0prle  38253  sge0p1  38266  sge0iunmptlemre  38267  sge0rpcpnf  38273  sge0rernmpt  38274  sge0isum  38279  sge0ad2en  38283  sge0xaddlem2  38286  sge0uzfsumgt  38296  omessre  38341  omeiunltfirp  38350  carageniuncllem2  38353  carageniuncl  38354  omege0  38364  omess0  38365  hoiprodcl  38379  ovnlerp  38394  ovnf  38395  ovn0lem  38397  ovnsubaddlem1  38402  hoiprodcl3  38412  hoidmvcl  38414  hoidmv1lelem3  38425  hoidmvlelem5  38431  ovnhoilem1  38433  xnn0xrge0  39086  xnn0xadd0  39098