Theorem 4re 8996

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 8980	. 2 ⊢ 4 = (3 + 1)
2		3re 8993	. . 3 ⊢ 3 ∈ ℝ
3		1re 7956	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7970	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5875  ℝcr 7810  1c1 7812   + caddc 7814  3c3 8971  4c4 8972

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 7905  ax-addrcl 7908

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

This theorem is referenced by:  4cn  8997  5re  8998  4ne0  9017  4ap0  9018  5pos  9019  2lt4  9092  1lt4  9093  4lt5  9094  3lt5  9095  2lt5  9096  1lt5  9097  4lt6  9099  3lt6  9100  4lt7  9105  3lt7  9106  4lt8  9112  3lt8  9113  4lt9  9120  3lt9  9121  8th4div3  9138  div4p1lem1div2  9172  4lt10  9519  3lt10  9520  eluz4eluz2  9567  fz0to4untppr  10124  fzo0to42pr  10220  fldiv4p1lem1div2  10305  faclbnd2  10722  4bc2eq6  10754  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemga  11032  sqrt2gt1lt2  11058  amgm2  11127  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos2bnd  11768  flodddiv4  11939  tsetndxnstarvndx  12649  slotsdifplendx  12665  slotsdifdsndx  12676  slotsdifunifndx  12683  cnfldstr  13460  dveflem  14190  sin0pilem2  14206  sinhalfpilem  14215  sincosq1lem  14249  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  pigt3  14268