Theorem 3re 9064

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 9050	. 2 |- 3 = ( 2 + 1 )
2		2re 9060	. . 3 |- 2 e. RR
3		1re 8025	. . 3 |- 1 e. RR
4	2, 3	readdcli 8039	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 3 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5922   RRcr 7878   1c1 7880   + caddc 7882   2c2 9041   3c3 9042

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9049  df-3 9050

This theorem is referenced by:  3cn  9065  4re  9067  3ne0  9085  3ap0  9086  4pos  9087  1lt3  9162  3lt4  9163  2lt4  9164  3lt5  9167  3lt6  9172  2lt6  9173  3lt7  9178  2lt7  9179  3lt8  9185  2lt8  9186  3lt9  9193  2lt9  9194  1le3  9202  8th4div3  9210  halfpm6th  9211  3halfnz  9423  3lt10  9593  2lt10  9594  uzuzle23  9645  uz3m2nn  9647  nn01to3  9691  3rp  9734  fz0to4untppr  10199  expnass  10737  sqrt9  11213  ef01bndlem  11921  sin01bnd  11922  cos2bnd  11925  sin01gt0  11927  cos01gt0  11928  egt2lt3  11945  flodddiv4  12101  starvndxnmulrndx  12821  scandxnmulrndx  12833  vscandxnmulrndx  12838  ipndxnmulrndx  12851  tsetndxnmulrndx  12870  plendxnmulrndx  12884  dsndxnmulrndx  12895  slotsdifunifndx  12905  dveflem  14962  sincosq3sgn  15064  sincosq4sgn  15065  cosq23lt0  15069  coseq0q4123  15070  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos6thpi  15078  pigt3  15080  pige3  15081  cos02pilt1  15087  lgsdir2lem1  15269  2lgslem3  15342  ex-fl  15371  ex-gcd  15377