Theorem 4re 9262

Description: The number 4 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
4re	⊢ 4 ∈ ℝ

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 9246	. 2 ⊢ 4 = (3 + 1)
2		3re 9259	. . 3 ⊢ 3 ∈ ℝ
3		1re 8221	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8235	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078  3c3 9237  4c4 9238

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 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9244  df-3 9245  df-4 9246

This theorem is referenced by:  4cn  9263  5re  9264  4ne0  9283  4ap0  9284  5pos  9285  2lt4  9359  1lt4  9360  4lt5  9361  3lt5  9362  2lt5  9363  1lt5  9364  4lt6  9366  3lt6  9367  4lt7  9372  3lt7  9373  4lt8  9379  3lt8  9380  4lt9  9387  3lt9  9388  8th4div3  9405  div4p1lem1div2  9440  4lt10  9790  3lt10  9791  uzuzle24  9841  uzuzle34  9842  eluz4eluz2  9846  fz0to4untppr  10404  fzo0to42pr  10511  fldiv4p1lem1div2  10611  faclbnd2  11050  4bc2eq6  11082  resqrexlemover  11633  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemnm  11641  resqrexlemga  11646  sqrt2gt1lt2  11672  amgm2  11741  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos2bnd  12384  flodddiv4  12560  4sqlem12  13038  tsetndxnstarvndx  13340  slotsdifplendx  13356  slotsdifdsndx  13371  slotsdifunifndx  13378  dveflem  15520  sin0pilem2  15576  sinhalfpilem  15585  sincosq1lem  15619  coseq0negpitopi  15630  tangtx  15632  sincos4thpi  15634  pigt3  15638  gausslemma2dlem0d  15854  gausslemma2dlem3  15865  gausslemma2dlem4  15866