Theorem 4re 9210

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 9194	. 2 ⊢ 4 = (3 + 1)
2		3re 9207	. . 3 ⊢ 3 ∈ ℝ
3		1re 8168	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8182	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  3c3 9185  4c4 9186

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9192  df-3 9193  df-4 9194

This theorem is referenced by:  4cn  9211  5re  9212  4ne0  9231  4ap0  9232  5pos  9233  2lt4  9307  1lt4  9308  4lt5  9309  3lt5  9310  2lt5  9311  1lt5  9312  4lt6  9314  3lt6  9315  4lt7  9320  3lt7  9321  4lt8  9327  3lt8  9328  4lt9  9335  3lt9  9336  8th4div3  9353  div4p1lem1div2  9388  4lt10  9736  3lt10  9737  uzuzle24  9787  uzuzle34  9788  eluz4eluz2  9792  fz0to4untppr  10349  fzo0to42pr  10455  fldiv4p1lem1div2  10555  faclbnd2  10994  4bc2eq6  11026  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemga  11574  sqrt2gt1lt2  11600  amgm2  11669  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos2bnd  12311  flodddiv4  12487  4sqlem12  12965  tsetndxnstarvndx  13267  slotsdifplendx  13283  slotsdifdsndx  13298  slotsdifunifndx  13305  dveflem  15440  sin0pilem2  15496  sinhalfpilem  15505  sincosq1lem  15539  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  pigt3  15558  gausslemma2dlem0d  15771  gausslemma2dlem3  15782  gausslemma2dlem4  15783