Theorem 4re 9148

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 9132	. 2 |- 4 = ( 3 + 1 )
2		3re 9145	. . 3 |- 3 e. RR
3		1re 8106	. . 3 |- 1 e. RR
4	2, 3	readdcli 8120	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2280	1 |- 4 e. RR

Syntax hints:   e. wcel 2178  (class class class)co 5967   RRcr 7959   1c1 7961   + caddc 7963   3c3 9123   4c4 9124

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203  df-2 9130  df-3 9131  df-4 9132

This theorem is referenced by:  4cn  9149  5re  9150  4ne0  9169  4ap0  9170  5pos  9171  2lt4  9245  1lt4  9246  4lt5  9247  3lt5  9248  2lt5  9249  1lt5  9250  4lt6  9252  3lt6  9253  4lt7  9258  3lt7  9259  4lt8  9265  3lt8  9266  4lt9  9273  3lt9  9274  8th4div3  9291  div4p1lem1div2  9326  4lt10  9674  3lt10  9675  eluz4eluz2  9723  fz0to4untppr  10281  fzo0to42pr  10386  fldiv4p1lem1div2  10485  faclbnd2  10924  4bc2eq6  10956  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemga  11449  sqrt2gt1lt2  11475  amgm2  11544  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos2bnd  12186  flodddiv4  12362  4sqlem12  12840  tsetndxnstarvndx  13141  slotsdifplendx  13157  slotsdifdsndx  13172  slotsdifunifndx  13179  dveflem  15313  sin0pilem2  15369  sinhalfpilem  15378  sincosq1lem  15412  coseq0negpitopi  15423  tangtx  15425  sincos4thpi  15427  pigt3  15431  gausslemma2dlem0d  15644  gausslemma2dlem3  15655  gausslemma2dlem4  15656