Theorem 6re 9031

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 9013	. 2 ⊢ 6 = (5 + 1)
2		5re 9029	. . 3 ⊢ 5 ∈ ℝ
3		1re 7987	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8001	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2262	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2160  (class class class)co 5897  ℝcr 7841  1c1 7843   + caddc 7845  5c5 9004  6c6 9005

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 2171  ax-1re 7936  ax-addrcl 7939

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9009  df-3 9010  df-4 9011  df-5 9012  df-6 9013

This theorem is referenced by:  6cn  9032  7re  9033  7pos  9052  4lt6  9130  3lt6  9131  2lt6  9132  1lt6  9133  6lt7  9134  5lt7  9135  6lt8  9141  5lt8  9142  6lt9  9149  5lt9  9150  8th4div3  9169  halfpm6th  9170  div4p1lem1div2  9203  6lt10  9548  5lt10  9549  5recm6rec  9558  efi4p  11760  resin4p  11761  recos4p  11762  ef01bndlem  11799  sin01bnd  11800  cos01bnd  11801  slotsdifipndx  12689  slotstnscsi  12709  plendxnvscandx  12723  slotsdnscsi  12733  sincos6thpi  14740  pigt3  14742