Theorem 6re 9318

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 9300	. 2 ⊢ 6 = (5 + 1)
2		5re 9316	. . 3 ⊢ 5 ∈ ℝ
3		1re 8273	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8287	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2305	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126  1c1 8128   + caddc 8130  5c5 9291  6c6 9292

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297  df-4 9298  df-5 9299  df-6 9300

This theorem is referenced by:  6cn  9319  7re  9320  7pos  9339  4lt6  9418  3lt6  9419  2lt6  9420  1lt6  9421  6lt7  9422  5lt7  9423  6lt8  9429  5lt8  9430  6lt9  9437  5lt9  9438  8th4div3  9457  halfpm6th  9458  div4p1lem1div2  9492  6lt10  9842  5lt10  9843  5recm6rec  9852  efi4p  12403  resin4p  12404  recos4p  12405  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  slotsdifipndx  13388  slotstnscsi  13408  plendxnvscandx  13422  slotsdnscsi  13436  sincos6thpi  15707  pigt3  15709