Theorem 0xr 8378

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 8375	. 2 |- RR C_ RR*
2		0re 8332	. 2 |- 0 e. RR
3	1, 2	sselii 3245	1 |- 0 e. RR*

This proof depends on syntax axioms:   e. wcel 2209   RRcr 8184   0cc0 8185   RR*cxr 8365

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 8279  ax-addrcl 8282  ax-rnegex 8294

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 8370

This theorem is used by:  0lepnf  10208  ge0gtmnf  10241  xlt0neg1  10256  xlt0neg2  10257  xle0neg1  10258  xle0neg2  10259  xaddf  10262  xaddval  10263  xaddid1  10280  xaddid2  10281  xnn0xadd0  10285  xaddge0  10296  xsubge0  10299  xposdif  10300  ioopos  10368  elxrge0  10396  0e0iccpnf  10398  dfrp2  10714  xrmaxadd  12051  xrminrpcl  12064  xrbdtri  12066  fprodge0  12428  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  sinltxirr  12552  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  sincos1sgn  12556  sincos2sgn  12557  cos12dec  12559  halfleoddlt  12685  psmetge0  15574  isxmet2d  15591  xmetge0  15608  blgt0  15645  xblss2ps  15647  xblss2  15648  xblm  15660  bdxmet  15744  bdmet  15745  bdmopn  15747  xmetxp  15750  cnblcld  15778  blssioo  15796  reeff1oleme  16015  reeff1o  16016  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  sinhalfpilem  16035  sincosq1lem  16069  sincosq1sgn  16070  sincosq2sgn  16071  sinq12gt0  16074  cosq14gt0  16076  tangtx  16082  sincos4thpi  16084  pigt3  16088  cosordlem  16094  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  repiecelem  17297  repiecege0  17299  iooref1o  17306  taupi  17347