Theorem 0xr 7836

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	⊢ 0 ∈ ℝ*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 7833	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 7790	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3099	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 1481  ℝcr 7643  0cc0 7644  ℝ^*cxr 7823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7738  ax-addrcl 7741  ax-rnegex 7753

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-xr 7828

This theorem is referenced by:  0lepnf  9606  ge0gtmnf  9636  xlt0neg1  9651  xlt0neg2  9652  xle0neg1  9653  xle0neg2  9654  xaddf  9657  xaddval  9658  xaddid1  9675  xaddid2  9676  xnn0xadd0  9680  xaddge0  9691  xsubge0  9694  xposdif  9695  ioopos  9763  elxrge0  9791  0e0iccpnf  9793  xrmaxadd  11062  xrminrpcl  11075  xrbdtri  11077  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  cos1bnd  11502  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  sincos1sgn  11507  sincos2sgn  11508  cos12dec  11510  halfleoddlt  11627  psmetge0  12539  isxmet2d  12556  xmetge0  12573  blgt0  12610  xblss2ps  12612  xblss2  12613  xblm  12625  bdxmet  12709  bdmet  12710  bdmopn  12712  xmetxp  12715  cnblcld  12743  blssioo  12753  reeff1oleme  12901  reeff1o  12902  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  sinhalfpilem  12920  sincosq1lem  12954  sincosq1sgn  12955  sincosq2sgn  12956  sinq12gt0  12959  cosq14gt0  12961  tangtx  12967  sincos4thpi  12969  pigt3  12973  cosordlem  12978  cosq34lt1  12979  cos02pilt1  12980  cos0pilt1  12981  iooref1o  13426  taupi  13430