Theorem 4re 9220

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  ℝcr 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  11575  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrexlemcalc3  11581  resqrexlemnm  11583  resqrexlemga  11588  sqrt2gt1lt2  11614  amgm2  11683  ef01bndlem  12322  sin01bnd  12323  cos01bnd  12324  cos2bnd  12326  flodddiv4  12502  4sqlem12  12980  tsetndxnstarvndx  13282  slotsdifplendx  13298  slotsdifdsndx  13313  slotsdifunifndx  13320  dveflem  15456  sin0pilem2  15512  sinhalfpilem  15521  sincosq1lem  15555  coseq0negpitopi  15566  tangtx  15568  sincos4thpi  15570  pigt3  15574  gausslemma2dlem0d  15787  gausslemma2dlem3  15798  gausslemma2dlem4  15799