Theorem 6re 9224

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 9206	. 2 ⊢ 6 = (5 + 1)
2		5re 9222	. . 3 ⊢ 5 ∈ ℝ
3		1re 8178	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8192	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031  1c1 8033   + caddc 8035  5c5 9197  6c6 9198

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202  df-3 9203  df-4 9204  df-5 9205  df-6 9206

This theorem is referenced by:  6cn  9225  7re  9226  7pos  9245  4lt6  9324  3lt6  9325  2lt6  9326  1lt6  9327  6lt7  9328  5lt7  9329  6lt8  9335  5lt8  9336  6lt9  9343  5lt9  9344  8th4div3  9363  halfpm6th  9364  div4p1lem1div2  9398  6lt10  9744  5lt10  9745  5recm6rec  9754  efi4p  12296  resin4p  12297  recos4p  12298  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  slotsdifipndx  13276  slotstnscsi  13296  plendxnvscandx  13310  slotsdnscsi  13324  sincos6thpi  15585  pigt3  15587