Theorem 4re 9115

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 9099	. 2 |- 4 = ( 3 + 1 )
2		3re 9112	. . 3 |- 3 e. RR
3		1re 8073	. . 3 |- 1 e. RR
4	2, 3	readdcli 8087	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2278	1 |- 4 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   3c3 9090   4c4 9091

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

This theorem is referenced by:  4cn  9116  5re  9117  4ne0  9136  4ap0  9137  5pos  9138  2lt4  9212  1lt4  9213  4lt5  9214  3lt5  9215  2lt5  9216  1lt5  9217  4lt6  9219  3lt6  9220  4lt7  9225  3lt7  9226  4lt8  9232  3lt8  9233  4lt9  9240  3lt9  9241  8th4div3  9258  div4p1lem1div2  9293  4lt10  9641  3lt10  9642  eluz4eluz2  9690  fz0to4untppr  10248  fzo0to42pr  10351  fldiv4p1lem1div2  10450  faclbnd2  10889  4bc2eq6  10921  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemcalc2  11359  resqrexlemcalc3  11360  resqrexlemnm  11362  resqrexlemga  11367  sqrt2gt1lt2  11393  amgm2  11462  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  cos2bnd  12104  flodddiv4  12280  4sqlem12  12758  tsetndxnstarvndx  13059  slotsdifplendx  13075  slotsdifdsndx  13090  slotsdifunifndx  13097  dveflem  15231  sin0pilem2  15287  sinhalfpilem  15296  sincosq1lem  15330  coseq0negpitopi  15341  tangtx  15343  sincos4thpi  15345  pigt3  15349  gausslemma2dlem0d  15562  gausslemma2dlem3  15573  gausslemma2dlem4  15574