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  11292  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrexlemcalc3  11298  resqrexlemnm  11300  resqrexlemga  11305  sqrt2gt1lt2  11331  amgm2  11400  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  cos2bnd  12042  flodddiv4  12218  4sqlem12  12696  tsetndxnstarvndx  12997  slotsdifplendx  13013  slotsdifdsndx  13028  slotsdifunifndx  13035  dveflem  15169  sin0pilem2  15225  sinhalfpilem  15234  sincosq1lem  15268  coseq0negpitopi  15279  tangtx  15281  sincos4thpi  15283  pigt3  15287  gausslemma2dlem0d  15500  gausslemma2dlem3  15511  gausslemma2dlem4  15512