Theorem 0xr 7730

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 7727	. 2 |- RR C_ RR*
2		0re 7684	. 2 |- 0 e. RR
3	1, 2	sselii 3058	1 |- 0 e. RR*

Syntax hints:   e. wcel 1461   RRcr 7540   0cc0 7541   RR*cxr 7717

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-1re 7633  ax-addrcl 7636  ax-rnegex 7648

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-xr 7722

This theorem is referenced by:  0lepnf  9463  ge0gtmnf  9493  xlt0neg1  9508  xlt0neg2  9509  xle0neg1  9510  xle0neg2  9511  xaddf  9514  xaddval  9515  xaddid1  9532  xaddid2  9533  xnn0xadd0  9537  xaddge0  9548  xsubge0  9551  xposdif  9552  ioopos  9620  elxrge0  9648  0e0iccpnf  9650  xrmaxadd  10916  xrminrpcl  10929  xrbdtri  10931  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  cos1bnd  11311  sin01gt0  11313  cos01gt0  11314  sin02gt0  11315  sincos1sgn  11316  sincos2sgn  11317  halfleoddlt  11433  psmetge0  12314  isxmet2d  12331  xmetge0  12348  blgt0  12385  xblss2ps  12387  xblss2  12388  xblm  12400  bdxmet  12484  bdmet  12485  bdmopn  12487  xmetxp  12490  cnblcld  12518  blssioo  12525