Theorem 4re 9219

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 9203	. 2 ⊢ 4 = (3 + 1)
2		3re 9216	. . 3 ⊢ 3 ∈ ℝ
3		1re 8177	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8191	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034  3c3 9194  4c4 9195

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 8125  ax-addrcl 8128

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

This theorem is referenced by:  4cn  9220  5re  9221  4ne0  9240  4ap0  9241  5pos  9242  2lt4  9316  1lt4  9317  4lt5  9318  3lt5  9319  2lt5  9320  1lt5  9321  4lt6  9323  3lt6  9324  4lt7  9329  3lt7  9330  4lt8  9336  3lt8  9337  4lt9  9344  3lt9  9345  8th4div3  9362  div4p1lem1div2  9397  4lt10  9745  3lt10  9746  uzuzle24  9796  uzuzle34  9797  eluz4eluz2  9801  fz0to4untppr  10358  fzo0to42pr  10464  fldiv4p1lem1div2  10564  faclbnd2  11003  4bc2eq6  11035  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemga  11583  sqrt2gt1lt2  11609  amgm2  11678  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos2bnd  12320  flodddiv4  12496  4sqlem12  12974  tsetndxnstarvndx  13276  slotsdifplendx  13292  slotsdifdsndx  13307  slotsdifunifndx  13314  dveflem  15449  sin0pilem2  15505  sinhalfpilem  15514  sincosq1lem  15548  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  pigt3  15567  gausslemma2dlem0d  15780  gausslemma2dlem3  15791  gausslemma2dlem4  15792