Theorem 6re 9214

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 9196	. 2 ⊢ 6 = (5 + 1)
2		5re 9212	. . 3 ⊢ 5 ∈ ℝ
3		1re 8168	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8182	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  5c5 9187  6c6 9188

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9192  df-3 9193  df-4 9194  df-5 9195  df-6 9196

This theorem is referenced by:  6cn  9215  7re  9216  7pos  9235  4lt6  9314  3lt6  9315  2lt6  9316  1lt6  9317  6lt7  9318  5lt7  9319  6lt8  9325  5lt8  9326  6lt9  9333  5lt9  9334  8th4div3  9353  halfpm6th  9354  div4p1lem1div2  9388  6lt10  9734  5lt10  9735  5recm6rec  9744  efi4p  12268  resin4p  12269  recos4p  12270  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  slotsdifipndx  13248  slotstnscsi  13268  plendxnvscandx  13282  slotsdnscsi  13296  sincos6thpi  15556  pigt3  15558