Theorem 4re 9026

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

Assertion

Ref	Expression
4re	|- 4 e. RR

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 9010	. 2 |- 4 = ( 3 + 1 )
2		3re 9023	. . 3 |- 3 e. RR
3		1re 7986	. . 3 |- 1 e. RR
4	2, 3	readdcli 8000	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2262	1 |- 4 e. RR

Syntax hints:   e. wcel 2160  (class class class)co 5896   RRcr 7840   1c1 7842   + caddc 7844   3c3 9001   4c4 9002

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 7935  ax-addrcl 7938

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9008  df-3 9009  df-4 9010

This theorem is referenced by:  4cn  9027  5re  9028  4ne0  9047  4ap0  9048  5pos  9049  2lt4  9122  1lt4  9123  4lt5  9124  3lt5  9125  2lt5  9126  1lt5  9127  4lt6  9129  3lt6  9130  4lt7  9135  3lt7  9136  4lt8  9142  3lt8  9143  4lt9  9150  3lt9  9151  8th4div3  9168  div4p1lem1div2  9202  4lt10  9549  3lt10  9550  eluz4eluz2  9597  fz0to4untppr  10154  fzo0to42pr  10250  fldiv4p1lem1div2  10336  faclbnd2  10754  4bc2eq6  10786  resqrexlemover  11051  resqrexlemcalc1  11055  resqrexlemcalc2  11056  resqrexlemcalc3  11057  resqrexlemnm  11059  resqrexlemga  11064  sqrt2gt1lt2  11090  amgm2  11159  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  cos2bnd  11800  flodddiv4  11971  4sqlem12  12434  tsetndxnstarvndx  12705  slotsdifplendx  12721  slotsdifdsndx  12732  slotsdifunifndx  12739  cnfldstr  13866  dveflem  14644  sin0pilem2  14660  sinhalfpilem  14669  sincosq1lem  14703  coseq0negpitopi  14714  tangtx  14716  sincos4thpi  14718  pigt3  14722