Theorem 6re 8914

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 8896	. 2 ⊢ 6 = (5 + 1)
2		5re 8912	. . 3 ⊢ 5 ∈ ℝ
3		1re 7877	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7891	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2230	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2128  (class class class)co 5824  ℝcr 7731  1c1 7733   + caddc 7735  5c5 8887  6c6 8888

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-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139  ax-1re 7826  ax-addrcl 7829

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-2 8892  df-3 8893  df-4 8894  df-5 8895  df-6 8896

This theorem is referenced by:  6cn  8915  7re  8916  7pos  8935  4lt6  9013  3lt6  9014  2lt6  9015  1lt6  9016  6lt7  9017  5lt7  9018  6lt8  9024  5lt8  9025  6lt9  9032  5lt9  9033  8th4div3  9052  halfpm6th  9053  div4p1lem1div2  9086  6lt10  9428  5lt10  9429  5recm6rec  9438  efi4p  11614  resin4p  11615  recos4p  11616  ef01bndlem  11653  sin01bnd  11654  cos01bnd  11655  sincos6thpi  13174  pigt3  13176