Theorem 6re 9117

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 9099	. 2 ⊢ 6 = (5 + 1)
2		5re 9115	. . 3 ⊢ 5 ∈ ℝ
3		1re 8071	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8085	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2278	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2176  (class class class)co 5944  ℝcr 7924  1c1 7926   + caddc 7928  5c5 9090  6c6 9091

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8019  ax-addrcl 8022

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9095  df-3 9096  df-4 9097  df-5 9098  df-6 9099

This theorem is referenced by:  6cn  9118  7re  9119  7pos  9138  4lt6  9217  3lt6  9218  2lt6  9219  1lt6  9220  6lt7  9221  5lt7  9222  6lt8  9228  5lt8  9229  6lt9  9236  5lt9  9237  8th4div3  9256  halfpm6th  9257  div4p1lem1div2  9291  6lt10  9637  5lt10  9638  5recm6rec  9647  efi4p  12028  resin4p  12029  recos4p  12030  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  slotsdifipndx  13007  slotstnscsi  13027  plendxnvscandx  13041  slotsdnscsi  13055  sincos6thpi  15314  pigt3  15316