Theorem 0xr 8073

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 8070	. 2 |- RR C_ RR*
2		0re 8026	. 2 |- 0 e. RR
3	1, 2	sselii 3180	1 |- 0 e. RR*

Syntax hints:   e. wcel 2167   RRcr 7878   0cc0 7879   RR*cxr 8060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7973  ax-addrcl 7976  ax-rnegex 7988

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-xr 8065

This theorem is referenced by:  0lepnf  9865  ge0gtmnf  9898  xlt0neg1  9913  xlt0neg2  9914  xle0neg1  9915  xle0neg2  9916  xaddf  9919  xaddval  9920  xaddid1  9937  xaddid2  9938  xnn0xadd0  9942  xaddge0  9953  xsubge0  9956  xposdif  9957  ioopos  10025  elxrge0  10053  0e0iccpnf  10055  dfrp2  10353  xrmaxadd  11426  xrminrpcl  11439  xrbdtri  11441  fprodge0  11802  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  sinltxirr  11926  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  sincos1sgn  11930  sincos2sgn  11931  cos12dec  11933  halfleoddlt  12059  psmetge0  14567  isxmet2d  14584  xmetge0  14601  blgt0  14638  xblss2ps  14640  xblss2  14641  xblm  14653  bdxmet  14737  bdmet  14738  bdmopn  14740  xmetxp  14743  cnblcld  14771  blssioo  14789  reeff1oleme  15008  reeff1o  15009  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  sinhalfpilem  15027  sincosq1lem  15061  sincosq1sgn  15062  sincosq2sgn  15063  sinq12gt0  15066  cosq14gt0  15068  tangtx  15074  sincos4thpi  15076  pigt3  15080  cosordlem  15085  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  iooref1o  15678  taupi  15717