Theorem 0xr 7945

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 7942	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 7899	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3139	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2136  ℝcr 7752  0cc0 7753  ℝ^*cxr 7932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7847  ax-addrcl 7850  ax-rnegex 7862

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-xr 7937

This theorem is referenced by:  0lepnf  9726  ge0gtmnf  9759  xlt0neg1  9774  xlt0neg2  9775  xle0neg1  9776  xle0neg2  9777  xaddf  9780  xaddval  9781  xaddid1  9798  xaddid2  9799  xnn0xadd0  9803  xaddge0  9814  xsubge0  9817  xposdif  9818  ioopos  9886  elxrge0  9914  0e0iccpnf  9916  dfrp2  10199  xrmaxadd  11202  xrminrpcl  11215  xrbdtri  11217  fprodge0  11578  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos1bnd  11700  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  sincos1sgn  11705  sincos2sgn  11706  cos12dec  11708  halfleoddlt  11831  psmetge0  12971  isxmet2d  12988  xmetge0  13005  blgt0  13042  xblss2ps  13044  xblss2  13045  xblm  13057  bdxmet  13141  bdmet  13142  bdmopn  13144  xmetxp  13147  cnblcld  13175  blssioo  13185  reeff1oleme  13333  reeff1o  13334  sin0pilem1  13342  sin0pilem2  13343  pilem3  13344  sinhalfpilem  13352  sincosq1lem  13386  sincosq1sgn  13387  sincosq2sgn  13388  sinq12gt0  13391  cosq14gt0  13393  tangtx  13399  sincos4thpi  13401  pigt3  13405  cosordlem  13410  cosq34lt1  13411  cos02pilt1  13412  cos0pilt1  13413  iooref1o  13913  taupi  13949