Theorem 6re 9065

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 9047	. 2 ⊢ 6 = (5 + 1)
2		5re 9063	. . 3 ⊢ 5 ∈ ℝ
3		1re 8020	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8034	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2266	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873  1c1 7875   + caddc 7877  5c5 9038  6c6 9039

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 7968  ax-addrcl 7971

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

This theorem is referenced by:  6cn  9066  7re  9067  7pos  9086  4lt6  9165  3lt6  9166  2lt6  9167  1lt6  9168  6lt7  9169  5lt7  9170  6lt8  9176  5lt8  9177  6lt9  9184  5lt9  9185  8th4div3  9204  halfpm6th  9205  div4p1lem1div2  9239  6lt10  9584  5lt10  9585  5recm6rec  9594  efi4p  11863  resin4p  11864  recos4p  11865  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  slotsdifipndx  12795  slotstnscsi  12815  plendxnvscandx  12829  slotsdnscsi  12839  sincos6thpi  15018  pigt3  15020