Theorem 0xr 8201

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	⊢ 0 ∈ ℝ*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 8198	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 8154	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3221	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2200  ℝcr 8006  0cc0 8007  ℝ^*cxr 8188

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 8101  ax-addrcl 8104  ax-rnegex 8116

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 8193

This theorem is referenced by:  0lepnf  9994  ge0gtmnf  10027  xlt0neg1  10042  xlt0neg2  10043  xle0neg1  10044  xle0neg2  10045  xaddf  10048  xaddval  10049  xaddid1  10066  xaddid2  10067  xnn0xadd0  10071  xaddge0  10082  xsubge0  10085  xposdif  10086  ioopos  10154  elxrge0  10182  0e0iccpnf  10184  dfrp2  10491  xrmaxadd  11780  xrminrpcl  11793  xrbdtri  11795  fprodge0  12156  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  cos1bnd  12278  sinltxirr  12280  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  sincos1sgn  12284  sincos2sgn  12285  cos12dec  12287  halfleoddlt  12413  psmetge0  15013  isxmet2d  15030  xmetge0  15047  blgt0  15084  xblss2ps  15086  xblss2  15087  xblm  15099  bdxmet  15183  bdmet  15184  bdmopn  15186  xmetxp  15189  cnblcld  15217  blssioo  15235  reeff1oleme  15454  reeff1o  15455  sin0pilem1  15463  sin0pilem2  15464  pilem3  15465  sinhalfpilem  15473  sincosq1lem  15507  sincosq1sgn  15508  sincosq2sgn  15509  sinq12gt0  15512  cosq14gt0  15514  tangtx  15520  sincos4thpi  15522  pigt3  15526  cosordlem  15531  cosq34lt1  15532  cos02pilt1  15533  cos0pilt1  15534  iooref1o  16432  taupi  16471