Theorem 0xr 8320

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 8317	. 2 |- RR C_ RR*
2		0re 8274	. 2 |- 0 e. RR
3	1, 2	sselii 3235	1 |- 0 e. RR*

Syntax hints:   e. wcel 2203   RRcr 8126   0cc0 8127   RR*cxr 8307

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 2214  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-xr 8312

This theorem is referenced by:  0lepnf  10123  ge0gtmnf  10156  xlt0neg1  10171  xlt0neg2  10172  xle0neg1  10173  xle0neg2  10174  xaddf  10177  xaddval  10178  xaddid1  10195  xaddid2  10196  xnn0xadd0  10200  xaddge0  10211  xsubge0  10214  xposdif  10215  ioopos  10283  elxrge0  10311  0e0iccpnf  10313  dfrp2  10623  xrmaxadd  11946  xrminrpcl  11959  xrbdtri  11961  fprodge0  12323  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  sinltxirr  12447  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  sincos1sgn  12451  sincos2sgn  12452  cos12dec  12454  halfleoddlt  12580  psmetge0  15196  isxmet2d  15213  xmetge0  15230  blgt0  15267  xblss2ps  15269  xblss2  15270  xblm  15282  bdxmet  15366  bdmet  15367  bdmopn  15369  xmetxp  15372  cnblcld  15400  blssioo  15418  reeff1oleme  15637  reeff1o  15638  sin0pilem1  15646  sin0pilem2  15647  pilem3  15648  sinhalfpilem  15656  sincosq1lem  15690  sincosq1sgn  15691  sincosq2sgn  15692  sinq12gt0  15695  cosq14gt0  15697  tangtx  15703  sincos4thpi  15705  pigt3  15709  cosordlem  15714  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  repiecelem  16809  repiecege0  16811  iooref1o  16818  taupi  16859