Theorem 0xr 8225

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 8222	. 2 |- RR C_ RR*
2		0re 8178	. 2 |- 0 e. RR
3	1, 2	sselii 3224	1 |- 0 e. RR*

Syntax hints:   e. wcel 2202   RRcr 8030   0cc0 8031   RR*cxr 8212

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-xr 8217

This theorem is referenced by:  0lepnf  10024  ge0gtmnf  10057  xlt0neg1  10072  xlt0neg2  10073  xle0neg1  10074  xle0neg2  10075  xaddf  10078  xaddval  10079  xaddid1  10096  xaddid2  10097  xnn0xadd0  10101  xaddge0  10112  xsubge0  10115  xposdif  10116  ioopos  10184  elxrge0  10212  0e0iccpnf  10214  dfrp2  10522  xrmaxadd  11821  xrminrpcl  11834  xrbdtri  11836  fprodge0  12197  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  sinltxirr  12321  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  sincos1sgn  12325  sincos2sgn  12326  cos12dec  12328  halfleoddlt  12454  psmetge0  15054  isxmet2d  15071  xmetge0  15088  blgt0  15125  xblss2ps  15127  xblss2  15128  xblm  15140  bdxmet  15224  bdmet  15225  bdmopn  15227  xmetxp  15230  cnblcld  15258  blssioo  15276  reeff1oleme  15495  reeff1o  15496  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  sinhalfpilem  15514  sincosq1lem  15548  sincosq1sgn  15549  sincosq2sgn  15550  sinq12gt0  15553  cosq14gt0  15555  tangtx  15561  sincos4thpi  15563  pigt3  15567  cosordlem  15572  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  iooref1o  16638  taupi  16677