Theorem 4re 9314

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 9298	. 2 |- 4 = ( 3 + 1 )
2		3re 9311	. . 3 |- 3 e. RR
3		1re 8273	. . 3 |- 1 e. RR
4	2, 3	readdcli 8287	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2305	1 |- 4 e. RR

Syntax hints:   e. wcel 2203  (class class class)co 6050   RRcr 8126   1c1 8128   + caddc 8130   3c3 9289   4c4 9290

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 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297  df-4 9298

This theorem is referenced by:  4cn  9315  5re  9316  4ne0  9335  4ap0  9336  5pos  9337  2lt4  9411  1lt4  9412  4lt5  9413  3lt5  9414  2lt5  9415  1lt5  9416  4lt6  9418  3lt6  9419  4lt7  9424  3lt7  9425  4lt8  9431  3lt8  9432  4lt9  9439  3lt9  9440  8th4div3  9457  div4p1lem1div2  9492  4lt10  9844  3lt10  9845  uzuzle24  9895  uzuzle34  9896  eluz4eluz2  9900  fz0to4untppr  10458  fzo0to42pr  10565  fldiv4p1lem1div2  10665  faclbnd2  11104  4bc2eq6  11137  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemga  11708  sqrt2gt1lt2  11734  amgm2  11803  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos2bnd  12446  flodddiv4  12622  4sqlem12  13100  tsetndxnstarvndx  13407  slotsdifplendx  13423  slotsdifdsndx  13438  slotsdifunifndx  13445  dveflem  15591  sin0pilem2  15647  sinhalfpilem  15656  sincosq1lem  15690  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  pigt3  15709  gausslemma2dlem0d  15925  gausslemma2dlem3  15936  gausslemma2dlem4  15937