Theorem 4re 8701

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 8685	. 2 |- 4 = ( 3 + 1 )
2		3re 8698	. . 3 |- 3 e. RR
3		1re 7683	. . 3 |- 1 e. RR
4	2, 3	readdcli 7697	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2185	1 |- 4 e. RR

Syntax hints:   e. wcel 1461  (class class class)co 5726   RRcr 7540   1c1 7542   + caddc 7544   3c3 8676   4c4 8677

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095  ax-1re 7633  ax-addrcl 7636

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109  df-2 8683  df-3 8684  df-4 8685

This theorem is referenced by:  4cn  8702  5re  8703  4ne0  8722  4ap0  8723  5pos  8724  2lt4  8791  1lt4  8792  4lt5  8793  3lt5  8794  2lt5  8795  1lt5  8796  4lt6  8798  3lt6  8799  4lt7  8804  3lt7  8805  4lt8  8811  3lt8  8812  4lt9  8819  3lt9  8820  8th4div3  8837  div4p1lem1div2  8871  4lt10  9215  3lt10  9216  fzo0to42pr  9884  fldiv4p1lem1div2  9965  faclbnd2  10375  4bc2eq6  10407  resqrexlemover  10668  resqrexlemcalc1  10672  resqrexlemcalc2  10673  resqrexlemcalc3  10674  resqrexlemnm  10676  resqrexlemga  10681  sqrt2gt1lt2  10707  amgm2  10776  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  cos2bnd  11312  flodddiv4  11473