Theorem 6re 9187

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 9169	. 2 ⊢ 6 = (5 + 1)
2		5re 9185	. . 3 ⊢ 5 ∈ ℝ
3		1re 8141	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8155	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994  1c1 7996   + caddc 7998  5c5 9160  6c6 9161

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 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9165  df-3 9166  df-4 9167  df-5 9168  df-6 9169

This theorem is referenced by:  6cn  9188  7re  9189  7pos  9208  4lt6  9287  3lt6  9288  2lt6  9289  1lt6  9290  6lt7  9291  5lt7  9292  6lt8  9298  5lt8  9299  6lt9  9306  5lt9  9307  8th4div3  9326  halfpm6th  9327  div4p1lem1div2  9361  6lt10  9707  5lt10  9708  5recm6rec  9717  efi4p  12223  resin4p  12224  recos4p  12225  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  slotsdifipndx  13203  slotstnscsi  13223  plendxnvscandx  13237  slotsdnscsi  13251  sincos6thpi  15510  pigt3  15512