Theorem 4re 9112

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 9096	. 2 ⊢ 4 = (3 + 1)
2		3re 9109	. . 3 ⊢ 3 ∈ ℝ
3		1re 8070	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8084	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2277	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  3c3 9087  4c4 9088

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094  df-3 9095  df-4 9096

This theorem is referenced by:  4cn  9113  5re  9114  4ne0  9133  4ap0  9134  5pos  9135  2lt4  9209  1lt4  9210  4lt5  9211  3lt5  9212  2lt5  9213  1lt5  9214  4lt6  9216  3lt6  9217  4lt7  9222  3lt7  9223  4lt8  9229  3lt8  9230  4lt9  9237  3lt9  9238  8th4div3  9255  div4p1lem1div2  9290  4lt10  9638  3lt10  9639  eluz4eluz2  9687  fz0to4untppr  10245  fzo0to42pr  10347  fldiv4p1lem1div2  10446  faclbnd2  10885  4bc2eq6  10917  resqrexlemover  11263  resqrexlemcalc1  11267  resqrexlemcalc2  11268  resqrexlemcalc3  11269  resqrexlemnm  11271  resqrexlemga  11276  sqrt2gt1lt2  11302  amgm2  11371  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos2bnd  12013  flodddiv4  12189  4sqlem12  12667  tsetndxnstarvndx  12968  slotsdifplendx  12984  slotsdifdsndx  12999  slotsdifunifndx  13006  dveflem  15140  sin0pilem2  15196  sinhalfpilem  15205  sincosq1lem  15239  coseq0negpitopi  15250  tangtx  15252  sincos4thpi  15254  pigt3  15258  gausslemma2dlem0d  15471  gausslemma2dlem3  15482  gausslemma2dlem4  15483