Theorem 4re 8426

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 8410	. 2 |- 4 = ( 3 + 1 )
2		3re 8423	. . 3 |- 3 e. RR
3		1re 7423	. . 3 |- 1 e. RR
4	2, 3	readdcli 7437	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2157	1 |- 4 e. RR

Syntax hints:   e. wcel 1436  (class class class)co 5606   RRcr 7285   1c1 7287   + caddc 7289   3c3 8400   4c4 8401

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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067  ax-1re 7375  ax-addrcl 7378

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081  df-2 8408  df-3 8409  df-4 8410

This theorem is referenced by:  4cn  8427  5re  8428  4ne0  8447  4ap0  8448  5pos  8449  2lt4  8515  1lt4  8516  4lt5  8517  3lt5  8518  2lt5  8519  1lt5  8520  4lt6  8522  3lt6  8523  4lt7  8528  3lt7  8529  4lt8  8535  3lt8  8536  4lt9  8543  3lt9  8544  8th4div3  8560  div4p1lem1div2  8594  4lt10  8936  3lt10  8937  fzo0to42pr  9551  fldiv4p1lem1div2  9632  faclbnd2  10038  4bc2eq6  10070  resqrexlemover  10330  resqrexlemcalc1  10334  resqrexlemcalc2  10335  resqrexlemcalc3  10336  resqrexlemnm  10338  resqrexlemga  10343  sqrt2gt1lt2  10369  amgm2  10438  flodddiv4  10800