Theorem 6re 9063

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 9045	. 2 ⊢ 6 = (5 + 1)
2		5re 9061	. . 3 ⊢ 5 ∈ ℝ
3		1re 8018	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8032	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2266	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5918  ℝcr 7871  1c1 7873   + caddc 7875  5c5 9036  6c6 9037

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9041  df-3 9042  df-4 9043  df-5 9044  df-6 9045

This theorem is referenced by:  6cn  9064  7re  9065  7pos  9084  4lt6  9162  3lt6  9163  2lt6  9164  1lt6  9165  6lt7  9166  5lt7  9167  6lt8  9173  5lt8  9174  6lt9  9181  5lt9  9182  8th4div3  9201  halfpm6th  9202  div4p1lem1div2  9236  6lt10  9581  5lt10  9582  5recm6rec  9591  efi4p  11860  resin4p  11861  recos4p  11862  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  slotsdifipndx  12792  slotstnscsi  12812  plendxnvscandx  12826  slotsdnscsi  12836  sincos6thpi  14977  pigt3  14979