Theorem 4re 8998

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 8982	. 2 |- 4 = ( 3 + 1 )
2		3re 8995	. . 3 |- 3 e. RR
3		1re 7958	. . 3 |- 1 e. RR
4	2, 3	readdcli 7972	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 4 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5877   RRcr 7812   1c1 7814   + caddc 7816   3c3 8973   4c4 8974

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8980  df-3 8981  df-4 8982

This theorem is referenced by:  4cn  8999  5re  9000  4ne0  9019  4ap0  9020  5pos  9021  2lt4  9094  1lt4  9095  4lt5  9096  3lt5  9097  2lt5  9098  1lt5  9099  4lt6  9101  3lt6  9102  4lt7  9107  3lt7  9108  4lt8  9114  3lt8  9115  4lt9  9122  3lt9  9123  8th4div3  9140  div4p1lem1div2  9174  4lt10  9521  3lt10  9522  eluz4eluz2  9569  fz0to4untppr  10126  fzo0to42pr  10222  fldiv4p1lem1div2  10307  faclbnd2  10724  4bc2eq6  10756  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemcalc2  11026  resqrexlemcalc3  11027  resqrexlemnm  11029  resqrexlemga  11034  sqrt2gt1lt2  11060  amgm2  11129  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos2bnd  11770  flodddiv4  11941  tsetndxnstarvndx  12654  slotsdifplendx  12670  slotsdifdsndx  12681  slotsdifunifndx  12688  cnfldstr  13496  dveflem  14226  sin0pilem2  14242  sinhalfpilem  14251  sincosq1lem  14285  coseq0negpitopi  14296  tangtx  14298  sincos4thpi  14300  pigt3  14304