Theorem 4re 8797

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 8781	. 2 |- 4 = ( 3 + 1 )
2		3re 8794	. . 3 |- 3 e. RR
3		1re 7765	. . 3 |- 1 e. RR
4	2, 3	readdcli 7779	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2212	1 |- 4 e. RR

Syntax hints:   e. wcel 1480  (class class class)co 5774   RRcr 7619   1c1 7621   + caddc 7623   3c3 8772   4c4 8773

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8779  df-3 8780  df-4 8781

This theorem is referenced by:  4cn  8798  5re  8799  4ne0  8818  4ap0  8819  5pos  8820  2lt4  8893  1lt4  8894  4lt5  8895  3lt5  8896  2lt5  8897  1lt5  8898  4lt6  8900  3lt6  8901  4lt7  8906  3lt7  8907  4lt8  8913  3lt8  8914  4lt9  8921  3lt9  8922  8th4div3  8939  div4p1lem1div2  8973  4lt10  9317  3lt10  9318  fzo0to42pr  9997  fldiv4p1lem1div2  10078  faclbnd2  10488  4bc2eq6  10520  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemga  10795  sqrt2gt1lt2  10821  amgm2  10890  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos2bnd  11467  flodddiv4  11631  dveflem  12855  sin0pilem2  12863  sinhalfpilem  12872  sincosq1lem  12906  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  pigt3  12925