Theorem 6re 8801

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 8783	. 2 ⊢ 6 = (5 + 1)
2		5re 8799	. . 3 ⊢ 5 ∈ ℝ
3		1re 7765	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7779	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2212	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5774  ℝcr 7619  1c1 7621   + caddc 7623  5c5 8774  6c6 8775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8779  df-3 8780  df-4 8781  df-5 8782  df-6 8783

This theorem is referenced by:  6cn  8802  7re  8803  7pos  8822  4lt6  8900  3lt6  8901  2lt6  8902  1lt6  8903  6lt7  8904  5lt7  8905  6lt8  8911  5lt8  8912  6lt9  8919  5lt9  8920  8th4div3  8939  halfpm6th  8940  div4p1lem1div2  8973  6lt10  9315  5lt10  9316  5recm6rec  9325  efi4p  11424  resin4p  11425  recos4p  11426  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sincos6thpi  12923  pigt3  12925