Theorem 6re 9119

Description: The number 6 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
6re	|- 6 e. RR

Proof of Theorem 6re

Step	Hyp	Ref	Expression
1		df-6 9101	. 2 |- 6 = ( 5 + 1 )
2		5re 9117	. . 3 |- 5 e. RR
3		1re 8073	. . 3 |- 1 e. RR
4	2, 3	readdcli 8087	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2278	1 |- 6 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   5c5 9092   6c6 9093

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 8021  ax-addrcl 8024

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

This theorem is referenced by:  6cn  9120  7re  9121  7pos  9140  4lt6  9219  3lt6  9220  2lt6  9221  1lt6  9222  6lt7  9223  5lt7  9224  6lt8  9230  5lt8  9231  6lt9  9238  5lt9  9239  8th4div3  9258  halfpm6th  9259  div4p1lem1div2  9293  6lt10  9639  5lt10  9640  5recm6rec  9649  efi4p  12061  resin4p  12062  recos4p  12063  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  slotsdifipndx  13040  slotstnscsi  13060  plendxnvscandx  13074  slotsdnscsi  13088  sincos6thpi  15347  pigt3  15349