Theorem 4re 9067

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 9051	. 2 ⊢ 4 = (3 + 1)
2		3re 9064	. . 3 ⊢ 3 ∈ ℝ
3		1re 8025	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8039	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878  1c1 7880   + caddc 7882  3c3 9042  4c4 9043

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 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9049  df-3 9050  df-4 9051

This theorem is referenced by:  4cn  9068  5re  9069  4ne0  9088  4ap0  9089  5pos  9090  2lt4  9164  1lt4  9165  4lt5  9166  3lt5  9167  2lt5  9168  1lt5  9169  4lt6  9171  3lt6  9172  4lt7  9177  3lt7  9178  4lt8  9184  3lt8  9185  4lt9  9192  3lt9  9193  8th4div3  9210  div4p1lem1div2  9245  4lt10  9592  3lt10  9593  eluz4eluz2  9641  fz0to4untppr  10199  fzo0to42pr  10296  fldiv4p1lem1div2  10395  faclbnd2  10834  4bc2eq6  10866  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemga  11188  sqrt2gt1lt2  11214  amgm2  11283  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos2bnd  11925  flodddiv4  12101  4sqlem12  12571  tsetndxnstarvndx  12871  slotsdifplendx  12887  slotsdifdsndx  12898  slotsdifunifndx  12905  dveflem  14962  sin0pilem2  15018  sinhalfpilem  15027  sincosq1lem  15061  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  pigt3  15080  gausslemma2dlem0d  15293  gausslemma2dlem3  15304  gausslemma2dlem4  15305