Theorem 6re 7996

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 7977	. 2 ⊢ 6 = (5 + 1)
2		5re 7994	. . 3 ⊢ 5 ∈ ℝ
3		1re 7026	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7040	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2110	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888  1c1 6890   + caddc 6892  5c5 7967  6c6 7968

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973  df-3 7974  df-4 7975  df-5 7976  df-6 7977

This theorem is referenced by:  6cn  7997  7re  7998  7pos  8018  4lt6  8097  3lt6  8098  2lt6  8099  1lt6  8100  6lt7  8101  5lt7  8102  6lt8  8108  5lt8  8109  6lt9  8116  5lt9  8117  6lt10  8125  5lt10  8126  8th4div3  8144  halfpm6th  8145  div4p1lem1div2  8177