Theorem 0xr 8325

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 8322	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 8279	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3237	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2205  ℝcr 8131  0cc0 8132  ℝ^*cxr 8312

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 8226  ax-addrcl 8229  ax-rnegex 8241

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 3217  df-in 3219  df-ss 3226  df-xr 8317

This theorem is referenced by:  0lepnf  10129  ge0gtmnf  10162  xlt0neg1  10177  xlt0neg2  10178  xle0neg1  10179  xle0neg2  10180  xaddf  10183  xaddval  10184  xaddid1  10201  xaddid2  10202  xnn0xadd0  10206  xaddge0  10217  xsubge0  10220  xposdif  10221  ioopos  10289  elxrge0  10317  0e0iccpnf  10319  dfrp2  10630  xrmaxadd  11954  xrminrpcl  11967  xrbdtri  11969  fprodge0  12331  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  cos1bnd  12453  sinltxirr  12455  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  sincos1sgn  12459  sincos2sgn  12460  cos12dec  12462  halfleoddlt  12588  psmetge0  15245  isxmet2d  15262  xmetge0  15279  blgt0  15316  xblss2ps  15318  xblss2  15319  xblm  15331  bdxmet  15415  bdmet  15416  bdmopn  15418  xmetxp  15421  cnblcld  15449  blssioo  15467  reeff1oleme  15686  reeff1o  15687  sin0pilem1  15695  sin0pilem2  15696  pilem3  15697  sinhalfpilem  15705  sincosq1lem  15739  sincosq1sgn  15740  sincosq2sgn  15741  sinq12gt0  15744  cosq14gt0  15746  tangtx  15752  sincos4thpi  15754  pigt3  15758  cosordlem  15763  cosq34lt1  15764  cos02pilt1  15765  cos0pilt1  15766  repiecelem  16858  repiecege0  16860  iooref1o  16867  taupi  16908