Theorem 4re 8889

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 8873	. 2 ⊢ 4 = (3 + 1)
2		3re 8886	. . 3 ⊢ 3 ∈ ℝ
3		1re 7856	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7870	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2227	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2125  (class class class)co 5814  ℝcr 7710  1c1 7712   + caddc 7714  3c3 8864  4c4 8865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2136  ax-1re 7805  ax-addrcl 7808

This theorem depends on definitions:  df-bi 116  df-cleq 2147  df-clel 2150  df-2 8871  df-3 8872  df-4 8873

This theorem is referenced by:  4cn  8890  5re  8891  4ne0  8910  4ap0  8911  5pos  8912  2lt4  8985  1lt4  8986  4lt5  8987  3lt5  8988  2lt5  8989  1lt5  8990  4lt6  8992  3lt6  8993  4lt7  8998  3lt7  8999  4lt8  9005  3lt8  9006  4lt9  9013  3lt9  9014  8th4div3  9031  div4p1lem1div2  9065  4lt10  9409  3lt10  9410  eluz4eluz2  9457  fzo0to42pr  10097  fldiv4p1lem1div2  10182  faclbnd2  10593  4bc2eq6  10625  resqrexlemover  10887  resqrexlemcalc1  10891  resqrexlemcalc2  10892  resqrexlemcalc3  10893  resqrexlemnm  10895  resqrexlemga  10900  sqrt2gt1lt2  10926  amgm2  10995  ef01bndlem  11630  sin01bnd  11631  cos01bnd  11632  cos2bnd  11634  flodddiv4  11798  dveflem  13034  sin0pilem2  13050  sinhalfpilem  13059  sincosq1lem  13093  coseq0negpitopi  13104  tangtx  13106  sincos4thpi  13108  pigt3  13112