Theorem 3re 8794

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

Assertion

Ref	Expression
3re	|- 3 e. RR

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 8780	. 2 |- 3 = ( 2 + 1 )
2		2re 8790	. . 3 |- 2 e. RR
3		1re 7765	. . 3 |- 1 e. RR
4	2, 3	readdcli 7779	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2212	1 |- 3 e. RR

Syntax hints:   e. wcel 1480  (class class class)co 5774   RRcr 7619   1c1 7621   + caddc 7623   2c2 8771   3c3 8772

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

This theorem is referenced by:  3cn  8795  4re  8797  3ne0  8815  3ap0  8816  4pos  8817  1lt3  8891  3lt4  8892  2lt4  8893  3lt5  8896  3lt6  8901  2lt6  8902  3lt7  8907  2lt7  8908  3lt8  8914  2lt8  8915  3lt9  8922  2lt9  8923  1le3  8931  8th4div3  8939  halfpm6th  8940  3halfnz  9148  3lt10  9318  2lt10  9319  uzuzle23  9366  uz3m2nn  9368  nn01to3  9409  3rp  9447  expnass  10398  sqrt9  10820  ef01bndlem  11463  sin01bnd  11464  cos2bnd  11467  sin01gt0  11468  cos01gt0  11469  egt2lt3  11486  flodddiv4  11631  dveflem  12855  sincosq3sgn  12909  sincosq4sgn  12910  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos6thpi  12923  pigt3  12925  pige3  12926  cos02pilt1  12932  ex-fl  12937  ex-gcd  12943