Theorem 3re 9381

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 9367	. 2 ⊢ 3 = (2 + 1)
2		2re 9377	. . 3 ⊢ 2 ∈ ℝ
3		1re 8326	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8340	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2311	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8179  1c1 8181   + caddc 8183  2c2 9358  3c3 9359

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 8274  ax-addrcl 8277

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

This theorem is used by:  3cn  9382  4re  9384  3ne0  9402  3ap0  9403  4pos  9404  1lt3  9481  3lt4  9482  2lt4  9483  3lt5  9486  3lt6  9491  2lt6  9492  3lt7  9497  2lt7  9498  3lt8  9504  2lt8  9505  3lt9  9512  2lt9  9513  1le3  9521  8th4div3  9529  halfpm6th  9530  3halfnz  9748  3lt10  9923  2lt10  9924  5eluz3  9971  uzuzle23  9972  uzuzle34  9974  uz3m2nn  9983  nn01to3  10027  3rp  10071  fz0to4untppr  10542  expnass  11097  sqrt9  11830  ef01bndlem  12542  sin01bnd  12543  cos2bnd  12546  sin01gt0  12548  cos01gt0  12549  egt2lt3  12566  flodddiv4  12722  starvndxnmulrndx  13551  scandxnmulrndx  13563  vscandxnmulrndx  13568  ipndxnmulrndx  13581  tsetndxnmulrndx  13600  plendxnmulrndx  13614  dsndxnmulrndx  13629  slotsdifunifndx  13639  dveflem  15918  sincosq3sgn  16021  sincosq4sgn  16022  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos6thpi  16035  pigt3  16037  pige3  16038  cos02pilt1  16044  log2tlbndlog2  16181  log2ublog2  16185  ppiqub  16254  chtqub  16257  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgsdir2lem1  16313  2lgslem3  16386  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem4  16898  ex-fl  16905  ex-gcd  16911