Theorem 0xr 8336

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 8333	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 8290	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3239	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2205  ℝcr 8142  0cc0 8143  ℝ^*cxr 8323

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-xr 8328

This theorem is referenced by:  0lepnf  10145  ge0gtmnf  10178  xlt0neg1  10193  xlt0neg2  10194  xle0neg1  10195  xle0neg2  10196  xaddf  10199  xaddval  10200  xaddid1  10217  xaddid2  10218  xnn0xadd0  10222  xaddge0  10233  xsubge0  10236  xposdif  10237  ioopos  10305  elxrge0  10333  0e0iccpnf  10335  dfrp2  10650  xrmaxadd  11974  xrminrpcl  11987  xrbdtri  11989  fprodge0  12351  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  cos1bnd  12473  sinltxirr  12475  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  sincos1sgn  12479  sincos2sgn  12480  cos12dec  12482  halfleoddlt  12608  psmetge0  15325  isxmet2d  15342  xmetge0  15359  blgt0  15396  xblss2ps  15398  xblss2  15399  xblm  15411  bdxmet  15495  bdmet  15496  bdmopn  15498  xmetxp  15501  cnblcld  15529  blssioo  15547  reeff1oleme  15766  reeff1o  15767  sin0pilem1  15775  sin0pilem2  15776  pilem3  15777  sinhalfpilem  15785  sincosq1lem  15819  sincosq1sgn  15820  sincosq2sgn  15821  sinq12gt0  15824  cosq14gt0  15826  tangtx  15832  sincos4thpi  15834  pigt3  15838  cosordlem  15843  cosq34lt1  15844  cos02pilt1  15845  cos0pilt1  15846  repiecelem  16948  repiecege0  16950  iooref1o  16957  taupi  16998