Theorem 6re 8938

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 8920	. 2 ⊢ 6 = (5 + 1)
2		5re 8936	. . 3 ⊢ 5 ∈ ℝ
3		1re 7898	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7912	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2239	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752  1c1 7754   + caddc 7756  5c5 8911  6c6 8912

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8916  df-3 8917  df-4 8918  df-5 8919  df-6 8920

This theorem is referenced by:  6cn  8939  7re  8940  7pos  8959  4lt6  9037  3lt6  9038  2lt6  9039  1lt6  9040  6lt7  9041  5lt7  9042  6lt8  9048  5lt8  9049  6lt9  9056  5lt9  9057  8th4div3  9076  halfpm6th  9077  div4p1lem1div2  9110  6lt10  9455  5lt10  9456  5recm6rec  9465  efi4p  11658  resin4p  11659  recos4p  11660  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sincos6thpi  13403  pigt3  13405