Theorem 0xr 8336

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 8333	. 2 |- RR C_ RR*
2		0re 8290	. 2 |- 0 e. RR
3	1, 2	sselii 3239	1 |- 0 e. RR*

Syntax hints:   e. wcel 2205   RRcr 8142   0cc0 8143   RR*cxr 8323

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-xr 8328

This theorem is referenced by:  0lepnf  10142  ge0gtmnf  10175  xlt0neg1  10190  xlt0neg2  10191  xle0neg1  10192  xle0neg2  10193  xaddf  10196  xaddval  10197  xaddid1  10214  xaddid2  10215  xnn0xadd0  10219  xaddge0  10230  xsubge0  10233  xposdif  10234  ioopos  10302  elxrge0  10330  0e0iccpnf  10332  dfrp2  10647  xrmaxadd  11971  xrminrpcl  11984  xrbdtri  11986  fprodge0  12348  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  sinltxirr  12472  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  sincos1sgn  12476  sincos2sgn  12477  cos12dec  12479  halfleoddlt  12605  psmetge0  15322  isxmet2d  15339  xmetge0  15356  blgt0  15393  xblss2ps  15395  xblss2  15396  xblm  15408  bdxmet  15492  bdmet  15493  bdmopn  15495  xmetxp  15498  cnblcld  15526  blssioo  15544  reeff1oleme  15763  reeff1o  15764  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  sinhalfpilem  15782  sincosq1lem  15816  sincosq1sgn  15817  sincosq2sgn  15818  sinq12gt0  15821  cosq14gt0  15823  tangtx  15829  sincos4thpi  15831  pigt3  15835  cosordlem  15840  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  repiecelem  16935  repiecege0  16937  iooref1o  16944  taupi  16985