Theorem 0xr 8379

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

This proof depends on syntax axioms:   ∈ wcel 2209  ℝcr 8185  0cc0 8186  ℝ^*cxr 8366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8280  ax-addrcl 8283  ax-rnegex 8295

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-xr 8371

This theorem is used by:  0lepnf  10210  ge0gtmnf  10243  xlt0neg1  10258  xlt0neg2  10259  xle0neg1  10260  xle0neg2  10261  xaddf  10264  xaddval  10265  xaddid1  10282  xaddid2  10283  xnn0xadd0  10287  xaddge0  10298  xsubge0  10301  xposdif  10302  ioopos  10370  elxrge0  10398  0e0iccpnf  10400  dfrp2  10716  xrmaxadd  12053  xrminrpcl  12066  xrbdtri  12068  fprodge0  12430  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  cos1bnd  12552  sinltxirr  12554  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  sincos1sgn  12558  sincos2sgn  12559  cos12dec  12561  halfleoddlt  12687  psmetge0  15569  isxmet2d  15586  xmetge0  15603  blgt0  15640  xblss2ps  15642  xblss2  15643  xblm  15655  bdxmet  15739  bdmet  15740  bdmopn  15742  xmetxp  15745  cnblcld  15773  blssioo  15791  reeff1oleme  16010  reeff1o  16011  sin0pilem1  16020  sin0pilem2  16021  pilem3  16022  sinhalfpilem  16030  sincosq1lem  16064  sincosq1sgn  16065  sincosq2sgn  16066  sinq12gt0  16069  cosq14gt0  16071  tangtx  16077  sincos4thpi  16079  pigt3  16083  cosordlem  16089  cosq34lt1  16090  cos02pilt1  16091  cos0pilt1  16092  repiecelem  17292  repiecege0  17294  iooref1o  17301  taupi  17342