Theorem 0xr 8006

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 8003	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 7959	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3154	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2148  ℝcr 7812  0cc0 7813  ℝ^*cxr 7993

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-xr 7998

This theorem is referenced by:  0lepnf  9792  ge0gtmnf  9825  xlt0neg1  9840  xlt0neg2  9841  xle0neg1  9842  xle0neg2  9843  xaddf  9846  xaddval  9847  xaddid1  9864  xaddid2  9865  xnn0xadd0  9869  xaddge0  9880  xsubge0  9883  xposdif  9884  ioopos  9952  elxrge0  9980  0e0iccpnf  9982  dfrp2  10266  xrmaxadd  11271  xrminrpcl  11284  xrbdtri  11286  fprodge0  11647  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos1bnd  11769  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  sincos1sgn  11774  sincos2sgn  11775  cos12dec  11777  halfleoddlt  11901  psmetge0  13916  isxmet2d  13933  xmetge0  13950  blgt0  13987  xblss2ps  13989  xblss2  13990  xblm  14002  bdxmet  14086  bdmet  14087  bdmopn  14089  xmetxp  14092  cnblcld  14120  blssioo  14130  reeff1oleme  14278  reeff1o  14279  sin0pilem1  14287  sin0pilem2  14288  pilem3  14289  sinhalfpilem  14297  sincosq1lem  14331  sincosq1sgn  14332  sincosq2sgn  14333  sinq12gt0  14336  cosq14gt0  14338  tangtx  14344  sincos4thpi  14346  pigt3  14350  cosordlem  14355  cosq34lt1  14356  cos02pilt1  14357  cos0pilt1  14358  iooref1o  14867  taupi  14906