Theorem 4re 9086

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 9070	. 2 ⊢ 4 = (3 + 1)
2		3re 9083	. . 3 ⊢ 3 ∈ ℝ
3		1re 8044	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8058	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897  1c1 7899   + caddc 7901  3c3 9061  4c4 9062

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9068  df-3 9069  df-4 9070

This theorem is referenced by:  4cn  9087  5re  9088  4ne0  9107  4ap0  9108  5pos  9109  2lt4  9183  1lt4  9184  4lt5  9185  3lt5  9186  2lt5  9187  1lt5  9188  4lt6  9190  3lt6  9191  4lt7  9196  3lt7  9197  4lt8  9203  3lt8  9204  4lt9  9211  3lt9  9212  8th4div3  9229  div4p1lem1div2  9264  4lt10  9611  3lt10  9612  eluz4eluz2  9660  fz0to4untppr  10218  fzo0to42pr  10315  fldiv4p1lem1div2  10414  faclbnd2  10853  4bc2eq6  10885  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemga  11207  sqrt2gt1lt2  11233  amgm2  11302  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos2bnd  11944  flodddiv4  12120  4sqlem12  12598  tsetndxnstarvndx  12898  slotsdifplendx  12914  slotsdifdsndx  12929  slotsdifunifndx  12936  dveflem  15070  sin0pilem2  15126  sinhalfpilem  15135  sincosq1lem  15169  coseq0negpitopi  15180  tangtx  15182  sincos4thpi  15184  pigt3  15188  gausslemma2dlem0d  15401  gausslemma2dlem3  15412  gausslemma2dlem4  15413