Theorem 4re 9220

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 9204	. 2 |- 4 = ( 3 + 1 )
2		3re 9217	. . 3 |- 3 e. RR
3		1re 8178	. . 3 |- 1 e. RR
4	2, 3	readdcli 8192	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 4 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035   3c3 9195   4c4 9196

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202  df-3 9203  df-4 9204

This theorem is referenced by:  4cn  9221  5re  9222  4ne0  9241  4ap0  9242  5pos  9243  2lt4  9317  1lt4  9318  4lt5  9319  3lt5  9320  2lt5  9321  1lt5  9322  4lt6  9324  3lt6  9325  4lt7  9330  3lt7  9331  4lt8  9337  3lt8  9338  4lt9  9345  3lt9  9346  8th4div3  9363  div4p1lem1div2  9398  4lt10  9746  3lt10  9747  uzuzle24  9797  uzuzle34  9798  eluz4eluz2  9802  fz0to4untppr  10359  fzo0to42pr  10466  fldiv4p1lem1div2  10566  faclbnd2  11005  4bc2eq6  11037  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemga  11601  sqrt2gt1lt2  11627  amgm2  11696  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos2bnd  12339  flodddiv4  12515  4sqlem12  12993  tsetndxnstarvndx  13295  slotsdifplendx  13311  slotsdifdsndx  13326  slotsdifunifndx  13333  dveflem  15469  sin0pilem2  15525  sinhalfpilem  15534  sincosq1lem  15568  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  pigt3  15587  gausslemma2dlem0d  15800  gausslemma2dlem3  15811  gausslemma2dlem4  15812