Theorem 4re 9279

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 9263	. 2 |- 4 = ( 3 + 1 )
2		3re 9276	. . 3 |- 3 e. RR
3		1re 8238	. . 3 |- 1 e. RR
4	2, 3	readdcli 8252	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 4 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095   3c3 9254   4c4 9255

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262  df-4 9263

This theorem is referenced by:  4cn  9280  5re  9281  4ne0  9300  4ap0  9301  5pos  9302  2lt4  9376  1lt4  9377  4lt5  9378  3lt5  9379  2lt5  9380  1lt5  9381  4lt6  9383  3lt6  9384  4lt7  9389  3lt7  9390  4lt8  9396  3lt8  9397  4lt9  9404  3lt9  9405  8th4div3  9422  div4p1lem1div2  9457  4lt10  9807  3lt10  9808  uzuzle24  9858  uzuzle34  9859  eluz4eluz2  9863  fz0to4untppr  10421  fzo0to42pr  10528  fldiv4p1lem1div2  10628  faclbnd2  11067  4bc2eq6  11099  resqrexlemover  11650  resqrexlemcalc1  11654  resqrexlemcalc2  11655  resqrexlemcalc3  11656  resqrexlemnm  11658  resqrexlemga  11663  sqrt2gt1lt2  11689  amgm2  11758  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  cos2bnd  12401  flodddiv4  12577  4sqlem12  13055  tsetndxnstarvndx  13357  slotsdifplendx  13373  slotsdifdsndx  13388  slotsdifunifndx  13395  dveflem  15537  sin0pilem2  15593  sinhalfpilem  15602  sincosq1lem  15636  coseq0negpitopi  15647  tangtx  15649  sincos4thpi  15651  pigt3  15655  gausslemma2dlem0d  15871  gausslemma2dlem3  15882  gausslemma2dlem4  15883