Theorem 4re 8934

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 8918	. 2 |- 4 = ( 3 + 1 )
2		3re 8931	. . 3 |- 3 e. RR
3		1re 7898	. . 3 |- 1 e. RR
4	2, 3	readdcli 7912	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2239	1 |- 4 e. RR

Syntax hints:   e. wcel 2136  (class class class)co 5842   RRcr 7752   1c1 7754   + caddc 7756   3c3 8909   4c4 8910

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8916  df-3 8917  df-4 8918

This theorem is referenced by:  4cn  8935  5re  8936  4ne0  8955  4ap0  8956  5pos  8957  2lt4  9030  1lt4  9031  4lt5  9032  3lt5  9033  2lt5  9034  1lt5  9035  4lt6  9037  3lt6  9038  4lt7  9043  3lt7  9044  4lt8  9050  3lt8  9051  4lt9  9058  3lt9  9059  8th4div3  9076  div4p1lem1div2  9110  4lt10  9457  3lt10  9458  eluz4eluz2  9505  fz0to4untppr  10059  fzo0to42pr  10155  fldiv4p1lem1div2  10240  faclbnd2  10655  4bc2eq6  10687  resqrexlemover  10952  resqrexlemcalc1  10956  resqrexlemcalc2  10957  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemga  10965  sqrt2gt1lt2  10991  amgm2  11060  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos2bnd  11701  flodddiv4  11871  dveflem  13327  sin0pilem2  13343  sinhalfpilem  13352  sincosq1lem  13386  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  pigt3  13405