Theorem 6re 8566

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 8548	. 2 ⊢ 6 = (5 + 1)
2		5re 8564	. . 3 ⊢ 5 ∈ ℝ
3		1re 7550	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7564	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2161	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 1439  (class class class)co 5668  ℝcr 7412  1c1 7414   + caddc 7416  5c5 8539  6c6 8540

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-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1re 7502  ax-addrcl 7505

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085  df-2 8544  df-3 8545  df-4 8546  df-5 8547  df-6 8548

This theorem is referenced by:  6cn  8567  7re  8568  7pos  8587  4lt6  8659  3lt6  8660  2lt6  8661  1lt6  8662  6lt7  8663  5lt7  8664  6lt8  8670  5lt8  8671  6lt9  8678  5lt9  8679  8th4div3  8698  halfpm6th  8699  div4p1lem1div2  8732  6lt10  9073  5lt10  9074  efi4p  11071  resin4p  11072  recos4p  11073  ef01bndlem  11110  sin01bnd  11111  cos01bnd  11112