Theorem 4re 8560

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 8544	. 2 ⊢ 4 = (3 + 1)
2		3re 8557	. . 3 ⊢ 3 ∈ ℝ
3		1re 7548	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7562	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2161	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 1439  (class class class)co 5666  ℝcr 7410  1c1 7412   + caddc 7414  3c3 8535  4c4 8536

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1re 7500  ax-addrcl 7503

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085  df-2 8542  df-3 8543  df-4 8544

This theorem is referenced by:  4cn  8561  5re  8562  4ne0  8581  4ap0  8582  5pos  8583  2lt4  8650  1lt4  8651  4lt5  8652  3lt5  8653  2lt5  8654  1lt5  8655  4lt6  8657  3lt6  8658  4lt7  8663  3lt7  8664  4lt8  8670  3lt8  8671  4lt9  8678  3lt9  8679  8th4div3  8696  div4p1lem1div2  8730  4lt10  9073  3lt10  9074  fzo0to42pr  9692  fldiv4p1lem1div2  9773  faclbnd2  10211  4bc2eq6  10243  resqrexlemover  10504  resqrexlemcalc1  10508  resqrexlemcalc2  10509  resqrexlemcalc3  10510  resqrexlemnm  10512  resqrexlemga  10517  sqrt2gt1lt2  10543  amgm2  10612  ef01bndlem  11108  sin01bnd  11109  cos01bnd  11110  cos2bnd  11112  flodddiv4  11273