Theorem 6re 9116

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 9098	. 2 ⊢ 6 = (5 + 1)
2		5re 9114	. . 3 ⊢ 5 ∈ ℝ
3		1re 8070	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8084	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2277	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  5c5 9089  6c6 9090

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094  df-3 9095  df-4 9096  df-5 9097  df-6 9098

This theorem is referenced by:  6cn  9117  7re  9118  7pos  9137  4lt6  9216  3lt6  9217  2lt6  9218  1lt6  9219  6lt7  9220  5lt7  9221  6lt8  9227  5lt8  9228  6lt9  9235  5lt9  9236  8th4div3  9255  halfpm6th  9256  div4p1lem1div2  9290  6lt10  9636  5lt10  9637  5recm6rec  9646  efi4p  11999  resin4p  12000  recos4p  12001  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  slotsdifipndx  12978  slotstnscsi  12998  plendxnvscandx  13012  slotsdnscsi  13026  sincos6thpi  15285  pigt3  15287