Theorem 0xr 8004

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 8001	. 2 |- RR C_ RR*
2		0re 7957	. 2 |- 0 e. RR
3	1, 2	sselii 3153	1 |- 0 e. RR*

Syntax hints:   e. wcel 2148   RRcr 7810   0cc0 7811   RR*cxr 7991

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 7905  ax-addrcl 7908  ax-rnegex 7920

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 2740  df-un 3134  df-in 3136  df-ss 3143  df-xr 7996

This theorem is referenced by:  0lepnf  9790  ge0gtmnf  9823  xlt0neg1  9838  xlt0neg2  9839  xle0neg1  9840  xle0neg2  9841  xaddf  9844  xaddval  9845  xaddid1  9862  xaddid2  9863  xnn0xadd0  9867  xaddge0  9878  xsubge0  9881  xposdif  9882  ioopos  9950  elxrge0  9978  0e0iccpnf  9980  dfrp2  10264  xrmaxadd  11269  xrminrpcl  11282  xrbdtri  11284  fprodge0  11645  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  sincos1sgn  11772  sincos2sgn  11773  cos12dec  11775  halfleoddlt  11899  psmetge0  13834  isxmet2d  13851  xmetge0  13868  blgt0  13905  xblss2ps  13907  xblss2  13908  xblm  13920  bdxmet  14004  bdmet  14005  bdmopn  14007  xmetxp  14010  cnblcld  14038  blssioo  14048  reeff1oleme  14196  reeff1o  14197  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  sinhalfpilem  14215  sincosq1lem  14249  sincosq1sgn  14250  sincosq2sgn  14251  sinq12gt0  14254  cosq14gt0  14256  tangtx  14262  sincos4thpi  14264  pigt3  14268  cosordlem  14273  cosq34lt1  14274  cos02pilt1  14275  cos0pilt1  14276  iooref1o  14785  taupi  14823