Theorem 4re 9084

Description: The number 4 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
4re	|- 4 e. RR

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 9068	. 2 |- 4 = ( 3 + 1 )
2		3re 9081	. . 3 |- 3 e. RR
3		1re 8042	. . 3 |- 1 e. RR
4	2, 3	readdcli 8056	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 4 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899   3c3 9059   4c4 9060

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 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9066  df-3 9067  df-4 9068

This theorem is referenced by:  4cn  9085  5re  9086  4ne0  9105  4ap0  9106  5pos  9107  2lt4  9181  1lt4  9182  4lt5  9183  3lt5  9184  2lt5  9185  1lt5  9186  4lt6  9188  3lt6  9189  4lt7  9194  3lt7  9195  4lt8  9201  3lt8  9202  4lt9  9209  3lt9  9210  8th4div3  9227  div4p1lem1div2  9262  4lt10  9609  3lt10  9610  eluz4eluz2  9658  fz0to4untppr  10216  fzo0to42pr  10313  fldiv4p1lem1div2  10412  faclbnd2  10851  4bc2eq6  10883  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemga  11205  sqrt2gt1lt2  11231  amgm2  11300  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos2bnd  11942  flodddiv4  12118  4sqlem12  12596  tsetndxnstarvndx  12896  slotsdifplendx  12912  slotsdifdsndx  12927  slotsdifunifndx  12934  dveflem  15046  sin0pilem2  15102  sinhalfpilem  15111  sincosq1lem  15145  coseq0negpitopi  15156  tangtx  15158  sincos4thpi  15160  pigt3  15164  gausslemma2dlem0d  15377  gausslemma2dlem3  15388  gausslemma2dlem4  15389