Theorem 4re 8172

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 8156	. 2 |- 4 = ( 3 + 1 )
2		3re 8169	. . 3 |- 3 e. RR
3		1re 7169	. . 3 |- 1 e. RR
4	2, 3	readdcli 7183	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2152	1 |- 4 e. RR

Syntax hints:   e. wcel 1434  (class class class)co 5537   RRcr 7031   1c1 7033   + caddc 7035   3c3 8146   4c4 8147

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1re 7121  ax-addrcl 7124

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-2 8154  df-3 8155  df-4 8156

This theorem is referenced by:  4cn  8173  5re  8174  4ne0  8193  4ap0  8194  5pos  8195  2lt4  8261  1lt4  8262  4lt5  8263  3lt5  8264  2lt5  8265  1lt5  8266  4lt6  8268  3lt6  8269  4lt7  8274  3lt7  8275  4lt8  8281  3lt8  8282  4lt9  8289  3lt9  8290  8th4div3  8306  div4p1lem1div2  8340  4lt10  8682  3lt10  8683  fzo0to42pr  9295  fldiv4p1lem1div2  9376  faclbnd2  9755  4bc2eq6  9787  resqrexlemover  10023  resqrexlemcalc1  10027  resqrexlemcalc2  10028  resqrexlemcalc3  10029  resqrexlemnm  10031  resqrexlemga  10036  sqrt2gt1lt2  10062  amgm2  10131  flodddiv4  10467