Theorem 3re 9259

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 9245	. 2 ⊢ 3 = (2 + 1)
2		2re 9255	. . 3 ⊢ 2 ∈ ℝ
3		1re 8221	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8235	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078  2c2 9236  3c3 9237

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9244  df-3 9245

This theorem is referenced by:  3cn  9260  4re  9262  3ne0  9280  3ap0  9281  4pos  9282  1lt3  9357  3lt4  9358  2lt4  9359  3lt5  9362  3lt6  9367  2lt6  9368  3lt7  9373  2lt7  9374  3lt8  9380  2lt8  9381  3lt9  9388  2lt9  9389  1le3  9397  8th4div3  9405  halfpm6th  9406  3halfnz  9621  3lt10  9791  2lt10  9792  5eluz3  9839  uzuzle23  9840  uzuzle34  9842  uz3m2nn  9851  nn01to3  9895  3rp  9938  fz0to4untppr  10404  expnass  10953  sqrt9  11671  ef01bndlem  12380  sin01bnd  12381  cos2bnd  12384  sin01gt0  12386  cos01gt0  12387  egt2lt3  12404  flodddiv4  12560  starvndxnmulrndx  13290  scandxnmulrndx  13302  vscandxnmulrndx  13307  ipndxnmulrndx  13320  tsetndxnmulrndx  13339  plendxnmulrndx  13353  dsndxnmulrndx  13368  slotsdifunifndx  13378  dveflem  15520  sincosq3sgn  15622  sincosq4sgn  15623  cosq23lt0  15627  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  sincos6thpi  15636  pigt3  15638  pige3  15639  cos02pilt1  15645  lgsdir2lem1  15830  2lgslem3  15903  konigsbergiedgwen  16408  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem4  16415  ex-fl  16422  ex-gcd  16428