Theorem 0xr 8362

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	|- 0 e. RR*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 8359	. 2 |- RR C_ RR*
2		0re 8316	. 2 |- 0 e. RR
3	1, 2	sselii 3245	1 |- 0 e. RR*

Syntax hints:   e. wcel 2209   RRcr 8168   0cc0 8169   RR*cxr 8349

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 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 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem 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 8354

This theorem is referenced by:  0lepnf  10171  ge0gtmnf  10204  xlt0neg1  10219  xlt0neg2  10220  xle0neg1  10221  xle0neg2  10222  xaddf  10225  xaddval  10226  xaddid1  10243  xaddid2  10244  xnn0xadd0  10248  xaddge0  10259  xsubge0  10262  xposdif  10263  ioopos  10331  elxrge0  10359  0e0iccpnf  10361  dfrp2  10676  xrmaxadd  12005  xrminrpcl  12018  xrbdtri  12020  fprodge0  12382  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  sinltxirr  12506  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  sincos1sgn  12510  sincos2sgn  12511  cos12dec  12513  halfleoddlt  12639  psmetge0  15355  isxmet2d  15372  xmetge0  15389  blgt0  15426  xblss2ps  15428  xblss2  15429  xblm  15441  bdxmet  15525  bdmet  15526  bdmopn  15528  xmetxp  15531  cnblcld  15559  blssioo  15577  reeff1oleme  15796  reeff1o  15797  sin0pilem1  15805  sin0pilem2  15806  pilem3  15807  sinhalfpilem  15815  sincosq1lem  15849  sincosq1sgn  15850  sincosq2sgn  15851  sinq12gt0  15854  cosq14gt0  15856  tangtx  15862  sincos4thpi  15864  pigt3  15868  cosordlem  15873  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  repiecelem  16979  repiecege0  16981  iooref1o  16988  taupi  17028