Theorem 0xr 8231

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 8228	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 8184	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3223	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2201  ℝcr 8036  0cc0 8037  ℝ^*cxr 8218

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-1re 8131  ax-addrcl 8134  ax-rnegex 8146

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-xr 8223

This theorem is referenced by:  0lepnf  10030  ge0gtmnf  10063  xlt0neg1  10078  xlt0neg2  10079  xle0neg1  10080  xle0neg2  10081  xaddf  10084  xaddval  10085  xaddid1  10102  xaddid2  10103  xnn0xadd0  10107  xaddge0  10118  xsubge0  10121  xposdif  10122  ioopos  10190  elxrge0  10218  0e0iccpnf  10220  dfrp2  10529  xrmaxadd  11844  xrminrpcl  11857  xrbdtri  11859  fprodge0  12221  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  cos1bnd  12343  sinltxirr  12345  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  sincos1sgn  12349  sincos2sgn  12350  cos12dec  12352  halfleoddlt  12478  psmetge0  15084  isxmet2d  15101  xmetge0  15118  blgt0  15155  xblss2ps  15157  xblss2  15158  xblm  15170  bdxmet  15254  bdmet  15255  bdmopn  15257  xmetxp  15260  cnblcld  15288  blssioo  15306  reeff1oleme  15525  reeff1o  15526  sin0pilem1  15534  sin0pilem2  15535  pilem3  15536  sinhalfpilem  15544  sincosq1lem  15578  sincosq1sgn  15579  sincosq2sgn  15580  sinq12gt0  15583  cosq14gt0  15585  tangtx  15591  sincos4thpi  15593  pigt3  15597  cosordlem  15602  cosq34lt1  15603  cos02pilt1  15604  cos0pilt1  15605  repiecelem  16696  repiecege0  16698  iooref1o  16705  taupi  16745