Theorem 4re 8994

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 8978	. 2 ⊢ 4 = (3 + 1)
2		3re 8991	. . 3 ⊢ 3 ∈ ℝ
3		1re 7955	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7969	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5874  ℝcr 7809  1c1 7811   + caddc 7813  3c3 8969  4c4 8970

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8976  df-3 8977  df-4 8978

This theorem is referenced by:  4cn  8995  5re  8996  4ne0  9015  4ap0  9016  5pos  9017  2lt4  9090  1lt4  9091  4lt5  9092  3lt5  9093  2lt5  9094  1lt5  9095  4lt6  9097  3lt6  9098  4lt7  9103  3lt7  9104  4lt8  9110  3lt8  9111  4lt9  9118  3lt9  9119  8th4div3  9136  div4p1lem1div2  9170  4lt10  9517  3lt10  9518  eluz4eluz2  9565  fz0to4untppr  10121  fzo0to42pr  10217  fldiv4p1lem1div2  10302  faclbnd2  10717  4bc2eq6  10749  resqrexlemover  11014  resqrexlemcalc1  11018  resqrexlemcalc2  11019  resqrexlemcalc3  11020  resqrexlemnm  11022  resqrexlemga  11027  sqrt2gt1lt2  11053  amgm2  11122  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  cos2bnd  11763  flodddiv4  11933  tsetndxnstarvndx  12643  slotsdifplendx  12659  slotsdifdsndx  12670  slotsdifunifndx  12677  cnfldstr  13388  dveflem  14118  sin0pilem2  14134  sinhalfpilem  14143  sincosq1lem  14177  coseq0negpitopi  14188  tangtx  14190  sincos4thpi  14192  pigt3  14196