Theorem 6re 8503

Description: The number 6 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
6re	⊢ 6 ∈ ℝ

Proof of Theorem 6re

Step	Hyp	Ref	Expression
1		df-6 8485	. 2 ⊢ 6 = (5 + 1)
2		5re 8501	. . 3 ⊢ 5 ∈ ℝ
3		1re 7487	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7501	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2160	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 1438  (class class class)co 5652  ℝcr 7349  1c1 7351   + caddc 7353  5c5 8476  6c6 8477

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7439  ax-addrcl 7442

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8481  df-3 8482  df-4 8483  df-5 8484  df-6 8485

This theorem is referenced by:  6cn  8504  7re  8505  7pos  8524  4lt6  8596  3lt6  8597  2lt6  8598  1lt6  8599  6lt7  8600  5lt7  8601  6lt8  8607  5lt8  8608  6lt9  8615  5lt9  8616  8th4div3  8635  halfpm6th  8636  div4p1lem1div2  8669  6lt10  9010  5lt10  9011  efi4p  11008  resin4p  11009  recos4p  11010  ef01bndlem  11047  sin01bnd  11048  cos01bnd  11049