Theorem 0xr 7998

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 7995	. 2 |- RR C_ RR*
2		0re 7952	. 2 |- 0 e. RR
3	1, 2	sselii 3152	1 |- 0 e. RR*

Syntax hints:   e. wcel 2148   RRcr 7805   0cc0 7806   RR*cxr 7985

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7900  ax-addrcl 7903  ax-rnegex 7915

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-xr 7990

This theorem is referenced by:  0lepnf  9784  ge0gtmnf  9817  xlt0neg1  9832  xlt0neg2  9833  xle0neg1  9834  xle0neg2  9835  xaddf  9838  xaddval  9839  xaddid1  9856  xaddid2  9857  xnn0xadd0  9861  xaddge0  9872  xsubge0  9875  xposdif  9876  ioopos  9944  elxrge0  9972  0e0iccpnf  9974  dfrp2  10257  xrmaxadd  11260  xrminrpcl  11273  xrbdtri  11275  fprodge0  11636  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  cos1bnd  11758  sin01gt0  11760  cos01gt0  11761  sin02gt0  11762  sincos1sgn  11763  sincos2sgn  11764  cos12dec  11766  halfleoddlt  11889  psmetge0  13613  isxmet2d  13630  xmetge0  13647  blgt0  13684  xblss2ps  13686  xblss2  13687  xblm  13699  bdxmet  13783  bdmet  13784  bdmopn  13786  xmetxp  13789  cnblcld  13817  blssioo  13827  reeff1oleme  13975  reeff1o  13976  sin0pilem1  13984  sin0pilem2  13985  pilem3  13986  sinhalfpilem  13994  sincosq1lem  14028  sincosq1sgn  14029  sincosq2sgn  14030  sinq12gt0  14033  cosq14gt0  14035  tangtx  14041  sincos4thpi  14043  pigt3  14047  cosordlem  14052  cosq34lt1  14053  cos02pilt1  14054  cos0pilt1  14055  iooref1o  14553  taupi  14591