Theorem 3re 9378

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

Assertion

Ref	Expression
3re	⊢ 3 ∈ ℝ

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 9364	. 2 ⊢ 3 = (2 + 1)
2		2re 9374	. . 3 ⊢ 2 ∈ ℝ
3		1re 8325	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8339	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2311	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178  1c1 8180   + caddc 8182  2c2 9355  3c3 9356

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 8273  ax-addrcl 8276

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

This theorem is used by:  3cn  9379  4re  9381  3ne0  9399  3ap0  9400  4pos  9401  1lt3  9476  3lt4  9477  2lt4  9478  3lt5  9481  3lt6  9486  2lt6  9487  3lt7  9492  2lt7  9493  3lt8  9499  2lt8  9500  3lt9  9507  2lt9  9508  1le3  9516  8th4div3  9524  halfpm6th  9525  3halfnz  9743  3lt10  9913  2lt10  9914  5eluz3  9961  uzuzle23  9962  uzuzle34  9964  uz3m2nn  9973  nn01to3  10017  3rp  10060  fz0to4untppr  10531  expnass  11082  sqrt9  11814  ef01bndlem  12523  sin01bnd  12524  cos2bnd  12527  sin01gt0  12529  cos01gt0  12530  egt2lt3  12547  flodddiv4  12703  starvndxnmulrndx  13498  scandxnmulrndx  13510  vscandxnmulrndx  13515  ipndxnmulrndx  13528  tsetndxnmulrndx  13547  plendxnmulrndx  13561  dsndxnmulrndx  13576  slotsdifunifndx  13586  dveflem  15827  sincosq3sgn  15929  sincosq4sgn  15930  cosq23lt0  15934  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos6thpi  15943  pigt3  15945  pige3  15946  cos02pilt1  15952  log2tlbndlog2  16082  log2ublog2  16086  lgsdir2lem1  16147  2lgslem3  16220  konigsbergiedgwen  16725  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem4  16732  ex-fl  16739  ex-gcd  16745