Theorem 4re 8497

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 8481	. 2 ⊢ 4 = (3 + 1)
2		3re 8494	. . 3 ⊢ 3 ∈ ℝ
3		1re 7485	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7499	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2160	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 1438  (class class class)co 5652  ℝcr 7347  1c1 7349   + caddc 7351  3c3 8472  4c4 8473

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7437  ax-addrcl 7440

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8479  df-3 8480  df-4 8481

This theorem is referenced by:  4cn  8498  5re  8499  4ne0  8518  4ap0  8519  5pos  8520  2lt4  8587  1lt4  8588  4lt5  8589  3lt5  8590  2lt5  8591  1lt5  8592  4lt6  8594  3lt6  8595  4lt7  8600  3lt7  8601  4lt8  8607  3lt8  8608  4lt9  8615  3lt9  8616  8th4div3  8633  div4p1lem1div2  8667  4lt10  9010  3lt10  9011  fzo0to42pr  9627  fldiv4p1lem1div2  9708  faclbnd2  10146  4bc2eq6  10178  resqrexlemover  10439  resqrexlemcalc1  10443  resqrexlemcalc2  10444  resqrexlemcalc3  10445  resqrexlemnm  10447  resqrexlemga  10452  sqrt2gt1lt2  10478  amgm2  10547  ef01bndlem  11043  sin01bnd  11044  cos01bnd  11045  cos2bnd  11047  flodddiv4  11208