Theorem 0xr 8003

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 8000	. 2 |- RR C_ RR*
2		0re 7956	. 2 |- 0 e. RR
3	1, 2	sselii 3152	1 |- 0 e. RR*

Syntax hints:   e. wcel 2148   RRcr 7809   0cc0 7810   RR*cxr 7990

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 7904  ax-addrcl 7907  ax-rnegex 7919

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-xr 7995

This theorem is referenced by:  0lepnf  9789  ge0gtmnf  9822  xlt0neg1  9837  xlt0neg2  9838  xle0neg1  9839  xle0neg2  9840  xaddf  9843  xaddval  9844  xaddid1  9861  xaddid2  9862  xnn0xadd0  9866  xaddge0  9877  xsubge0  9880  xposdif  9881  ioopos  9949  elxrge0  9977  0e0iccpnf  9979  dfrp2  10263  xrmaxadd  11268  xrminrpcl  11281  xrbdtri  11283  fprodge0  11644  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  cos1bnd  11766  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  sincos1sgn  11771  sincos2sgn  11772  cos12dec  11774  halfleoddlt  11898  psmetge0  13767  isxmet2d  13784  xmetge0  13801  blgt0  13838  xblss2ps  13840  xblss2  13841  xblm  13853  bdxmet  13937  bdmet  13938  bdmopn  13940  xmetxp  13943  cnblcld  13971  blssioo  13981  reeff1oleme  14129  reeff1o  14130  sin0pilem1  14138  sin0pilem2  14139  pilem3  14140  sinhalfpilem  14148  sincosq1lem  14182  sincosq1sgn  14183  sincosq2sgn  14184  sinq12gt0  14187  cosq14gt0  14189  tangtx  14195  sincos4thpi  14197  pigt3  14201  cosordlem  14206  cosq34lt1  14207  cos02pilt1  14208  cos0pilt1  14209  iooref1o  14718  taupi  14756