Theorem 0xr 8161

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 8158	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 8114	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3201	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2180  ℝcr 7966  0cc0 7967  ℝ^*cxr 8148

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-1re 8061  ax-addrcl 8064  ax-rnegex 8076

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-xr 8153

This theorem is referenced by:  0lepnf  9954  ge0gtmnf  9987  xlt0neg1  10002  xlt0neg2  10003  xle0neg1  10004  xle0neg2  10005  xaddf  10008  xaddval  10009  xaddid1  10026  xaddid2  10027  xnn0xadd0  10031  xaddge0  10042  xsubge0  10045  xposdif  10046  ioopos  10114  elxrge0  10142  0e0iccpnf  10144  dfrp2  10450  xrmaxadd  11738  xrminrpcl  11751  xrbdtri  11753  fprodge0  12114  ef01bndlem  12233  sin01bnd  12234  cos01bnd  12235  cos1bnd  12236  sinltxirr  12238  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  sincos1sgn  12242  sincos2sgn  12243  cos12dec  12245  halfleoddlt  12371  psmetge0  14970  isxmet2d  14987  xmetge0  15004  blgt0  15041  xblss2ps  15043  xblss2  15044  xblm  15056  bdxmet  15140  bdmet  15141  bdmopn  15143  xmetxp  15146  cnblcld  15174  blssioo  15192  reeff1oleme  15411  reeff1o  15412  sin0pilem1  15420  sin0pilem2  15421  pilem3  15422  sinhalfpilem  15430  sincosq1lem  15464  sincosq1sgn  15465  sincosq2sgn  15466  sinq12gt0  15469  cosq14gt0  15471  tangtx  15477  sincos4thpi  15479  pigt3  15483  cosordlem  15488  cosq34lt1  15489  cos02pilt1  15490  cos0pilt1  15491  iooref1o  16313  taupi  16352