Theorem 3re 9387

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 9373	. 2 |- 3 = ( 2 + 1 )
2		2re 9383	. . 3 |- 2 e. RR
3		1re 8331	. . 3 |- 1 e. RR
4	2, 3	readdcli 8345	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2311	1 |- 3 e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6088   RRcr 8184   1c1 8186   + caddc 8188   2c2 9364   3c3 9365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1re 8279  ax-addrcl 8282

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9372  df-3 9373

This theorem is used by:  3cn  9388  4re  9390  3ne0  9408  3ap0  9409  4pos  9410  1lt3  9487  3lt4  9488  2lt4  9489  3lt5  9492  3lt6  9497  2lt6  9498  3lt7  9503  2lt7  9504  3lt8  9510  2lt8  9511  3lt9  9518  2lt9  9519  1le3  9527  8th4div3  9535  halfpm6th  9536  3halfnz  9754  3lt10  9929  2lt10  9930  5eluz3  9977  uzuzle23  9978  uzuzle34  9980  uz3m2nn  9989  nn01to3  10033  3rp  10077  fz0to4untppr  10548  expnass  11103  sqrt9  11836  ef01bndlem  12548  sin01bnd  12549  cos2bnd  12552  sin01gt0  12554  cos01gt0  12555  egt2lt3  12572  flodddiv4  12728  starvndxnmulrndx  13557  scandxnmulrndx  13569  vscandxnmulrndx  13574  ipndxnmulrndx  13587  tsetndxnmulrndx  13606  plendxnmulrndx  13620  dsndxnmulrndx  13635  slotsdifunifndx  13645  dveflem  15952  sincosq3sgn  16055  sincosq4sgn  16056  cosq23lt0  16060  coseq0q4123  16061  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos6thpi  16069  pigt3  16071  pige3  16072  cos02pilt1  16079  log2tlbndlog2  16220  log2ublog2  16224  ppiqub  16293  chtqub  16296  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgsdir2lem1  16352  2lgslem3  16425  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem4  16937  ex-fl  16944  ex-gcd  16950