Theorem 0xr 9418

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 9415	. 2 |- RR C_ RR*
2		0re 9374	. 2 |- 0 e. RR
3	1, 2	sselii 3341	1 |- 0 e. RR*

Syntax hints:   e. wcel 1755   RRcr 9269   0cc0 9270   RR*cxr 9405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-xr 9410

This theorem is referenced by:  0lepnf  11099  ge0gtmnf  11132  max0sub  11154  xlt0neg1  11177  xlt0neg2  11178  xle0neg1  11179  xle0neg2  11180  xaddf  11182  xaddid1  11197  xaddid2  11198  xaddge0  11209  xsubge0  11212  xposdif  11213  xmullem  11215  xmullem2  11216  xmul01  11218  xmul02  11219  xmulneg1  11220  xmulf  11223  xmulpnf1  11225  xmulasslem2  11233  xmulge0  11235  xmulasslem  11236  xlemul1a  11239  xadddi  11246  xadddi2  11248  ioopos  11360  ioorebas  11379  elxrge0  11381  0e0iccpnf  11383  xov1plusxeqvd  11418  rpsup  11689  hashgt0  12135  hashle00  12142  hashgt0elex  12143  sgn0  12562  sgnp  12563  sgnn  12567  ef01bndlem  13451  sin01bnd  13452  cos01bnd  13453  cos1bnd  13454  sinltx  13456  sin01gt0  13457  cos01gt0  13458  sin02gt0  13459  sincos1sgn  13460  sincos2sgn  13461  leordtval2  18658  pnfnei  18666  mnfnei  18667  psmetge0  19730  isxmet2d  19744  xmetge0  19761  xmetgt0  19775  prdsdsf  19784  prdsxmetlem  19785  xpsdsval  19798  blgt0  19816  xblss2ps  19818  xblss2  19819  xbln0  19831  prdsbl  19908  stdbdxmet  19932  stdbdmopn  19935  metusttoOLD  19974  metustto  19975  metustidOLD  19976  metustid  19977  metustexhalfOLD  19980  metustexhalf  19981  cfilucfilOLD  19986  cfilucfil  19987  blval2  19992  metuel2  19996  nmoge0  20142  nmo0  20156  cnblcld  20196  blssioo  20214  blcvx  20217  xrsxmet  20228  metdsf  20266  metds0  20268  metdseq0  20272  metnrmlem1a  20276  iccpnfcnv  20358  iccpnfhmeo  20359  xrhmeo  20360  pcoass  20438  iscfil2  20619  ovolmge0  20802  ovolge0  20806  ovolf  20807  ovolssnul  20812  ovolctb  20815  ovoliunnul  20832  ovolicopnf  20849  voliunlem3  20875  volsup  20879  ioorf  20895  volivth  20929  vitalilem4  20933  vitalilem5  20934  itg2ge0  21055  itg2const2  21061  itg2seq  21062  itg2monolem1  21070  itg2monolem2  21071  itg2monolem3  21072  itg2gt0  21080  dvne0  21325  mdegle0  21433  ply1remlem  21519  ply1rem  21520  plypf1  21565  aaliou3lem2  21694  aaliou3lem3  21695  taylfvallem1  21707  taylfval  21709  tayl0  21712  radcnvcl  21767  radcnvle  21770  pserulm  21772  psercnlem1  21775  pilem2  21802  sinhalfpilem  21810  sincosq1lem  21844  sincosq1sgn  21845  sincosq2sgn  21846  tangtx  21852  tanabsge  21853  sinq12gt0  21854  cosq14gt0  21857  sincos4thpi  21860  pige3  21864  cosordlem  21872  tanord1  21878  tanord  21879  efifo  21888  argimgt0  21946  argimlt0  21947  logccv  21993  loglesqr  22081  atantan  22203  rlimcnp  22244  rlimcnp2  22245  scvxcvx  22264  basellem1  22303  dchrisum0lem2a  22651  pntibndlem1  22723  pntibnd  22727  pntlemc  22729  pntlem3  22743  abvcxp  22749  padicabvf  22765  padicabvcxp  22766  ostth2  22771  ttgcontlem1  22954  nmooge0  23990  nmoo0  24014  nmlnogt0  24020  nmopge0  25138  nmopgt0  25139  nmfnge0  25154  nmop0  25213  nmfn0  25214  xraddge02  25875  xlt2addrd  25876  elxrge02  25930  xrs0  25959  xrge00  25970  xrge0addass  25974  xrge0neqmnf  25975  xrge0addgt0  25977  xrge0adddir  25979  fsumrp0cl  25982  metider  26175  unitssxrge0  26184  xrge0iifcnv  26217  xrge0iifcv  26218  xrge0iifiso  26219  xrge0iifhom  26221  xrge0mulc1cn  26225  pnfneige0  26235  lmxrge0  26236  esumnul  26356  esum0  26357  esumle  26362  esumlef  26367  esumcst  26368  esumsn  26369  esumpr2  26371  esumpinfval  26376  esumpinfsum  26380  esumpcvgval  26381  esumpmono  26382  hashf2  26387  esumcvg  26389  measle0  26476  voliune  26499  volfiniune  26500  ddemeas  26506  aean  26514  prob01  26644  probmeasb  26661  dstfrvclim1  26708  sgncl  26769  sgn3da  26772  sgn0bi  26778  cvmliftlem10  27031  cvmliftlem13  27033  sinccvglem  27164  sin2h  28266  tan2h  28268  mblfinlem2  28273  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  mbfposadd  28283  itg2addnclem2  28288  itg2gt0cn  28291  ftc1anclem5  28315  ftc1anclem8  28318  dvasin  28324  areacirc  28333  rrnequiv  28578  idomrootle  29405  itgsin0pilem1  29636  stoweidlem46  29687  bj-flbi3  32128