Theorem 6re 9002

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 8984	. 2 ⊢ 6 = (5 + 1)
2		5re 9000	. . 3 ⊢ 5 ∈ ℝ
3		1re 7958	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7972	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812  1c1 7814   + caddc 7816  5c5 8975  6c6 8976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8980  df-3 8981  df-4 8982  df-5 8983  df-6 8984

This theorem is referenced by:  6cn  9003  7re  9004  7pos  9023  4lt6  9101  3lt6  9102  2lt6  9103  1lt6  9104  6lt7  9105  5lt7  9106  6lt8  9112  5lt8  9113  6lt9  9120  5lt9  9121  8th4div3  9140  halfpm6th  9141  div4p1lem1div2  9174  6lt10  9519  5lt10  9520  5recm6rec  9529  efi4p  11727  resin4p  11728  recos4p  11729  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  slotsdifipndx  12635  slotstnscsi  12655  plendxnvscandx  12669  slotsdnscsi  12679  sincos6thpi  14348  pigt3  14350