Theorem 0xr 8193

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 8190	. 2 |- RR C_ RR*
2		0re 8146	. 2 |- 0 e. RR
3	1, 2	sselii 3221	1 |- 0 e. RR*

Syntax hints:   e. wcel 2200   RRcr 7998   0cc0 7999   RR*cxr 8180

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-xr 8185

This theorem is referenced by:  0lepnf  9986  ge0gtmnf  10019  xlt0neg1  10034  xlt0neg2  10035  xle0neg1  10036  xle0neg2  10037  xaddf  10040  xaddval  10041  xaddid1  10058  xaddid2  10059  xnn0xadd0  10063  xaddge0  10074  xsubge0  10077  xposdif  10078  ioopos  10146  elxrge0  10174  0e0iccpnf  10176  dfrp2  10483  xrmaxadd  11772  xrminrpcl  11785  xrbdtri  11787  fprodge0  12148  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos1bnd  12270  sinltxirr  12272  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  sincos1sgn  12276  sincos2sgn  12277  cos12dec  12279  halfleoddlt  12405  psmetge0  15005  isxmet2d  15022  xmetge0  15039  blgt0  15076  xblss2ps  15078  xblss2  15079  xblm  15091  bdxmet  15175  bdmet  15176  bdmopn  15178  xmetxp  15181  cnblcld  15209  blssioo  15227  reeff1oleme  15446  reeff1o  15447  sin0pilem1  15455  sin0pilem2  15456  pilem3  15457  sinhalfpilem  15465  sincosq1lem  15499  sincosq1sgn  15500  sincosq2sgn  15501  sinq12gt0  15504  cosq14gt0  15506  tangtx  15512  sincos4thpi  15514  pigt3  15518  cosordlem  15523  cosq34lt1  15524  cos02pilt1  15525  cos0pilt1  15526  iooref1o  16402  taupi  16441