Theorem 6re 9283

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 9265	. 2 ⊢ 6 = (5 + 1)
2		5re 9281	. . 3 ⊢ 5 ∈ ℝ
3		1re 8238	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8252	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8091  1c1 8093   + caddc 8095  5c5 9256  6c6 9257

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262  df-4 9263  df-5 9264  df-6 9265

This theorem is referenced by:  6cn  9284  7re  9285  7pos  9304  4lt6  9383  3lt6  9384  2lt6  9385  1lt6  9386  6lt7  9387  5lt7  9388  6lt8  9394  5lt8  9395  6lt9  9402  5lt9  9403  8th4div3  9422  halfpm6th  9423  div4p1lem1div2  9457  6lt10  9805  5lt10  9806  5recm6rec  9815  efi4p  12358  resin4p  12359  recos4p  12360  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  slotsdifipndx  13338  slotstnscsi  13358  plendxnvscandx  13372  slotsdnscsi  13386  sincos6thpi  15653  pigt3  15655