Theorem 3re 8991

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 8977	. 2 |- 3 = ( 2 + 1 )
2		2re 8987	. . 3 |- 2 e. RR
3		1re 7955	. . 3 |- 1 e. RR
4	2, 3	readdcli 7969	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 3 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5874   RRcr 7809   1c1 7811   + caddc 7813   2c2 8968   3c3 8969

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 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8976  df-3 8977

This theorem is referenced by:  3cn  8992  4re  8994  3ne0  9012  3ap0  9013  4pos  9014  1lt3  9088  3lt4  9089  2lt4  9090  3lt5  9093  3lt6  9098  2lt6  9099  3lt7  9104  2lt7  9105  3lt8  9111  2lt8  9112  3lt9  9119  2lt9  9120  1le3  9128  8th4div3  9136  halfpm6th  9137  3halfnz  9348  3lt10  9518  2lt10  9519  uzuzle23  9569  uz3m2nn  9571  nn01to3  9615  3rp  9657  fz0to4untppr  10121  expnass  10622  sqrt9  11052  ef01bndlem  11759  sin01bnd  11760  cos2bnd  11763  sin01gt0  11764  cos01gt0  11765  egt2lt3  11782  flodddiv4  11933  starvndxnmulrndx  12596  scandxnmulrndx  12608  vscandxnmulrndx  12613  ipndxnmulrndx  12626  tsetndxnmulrndx  12642  plendxnmulrndx  12656  dsndxnmulrndx  12667  slotsdifunifndx  12677  dveflem  14080  sincosq3sgn  14142  sincosq4sgn  14143  cosq23lt0  14147  coseq0q4123  14148  coseq00topi  14149  coseq0negpitopi  14150  tangtx  14152  sincos6thpi  14156  pigt3  14158  pige3  14159  cos02pilt1  14165  lgsdir2lem1  14322  ex-fl  14359  ex-gcd  14365