Theorem 3re 9387

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℝcr 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  9753  3lt10  9928  2lt10  9929  5eluz3  9976  uzuzle23  9977  uzuzle34  9979  uz3m2nn  9988  nn01to3  10032  3rp  10076  fz0to4untppr  10547  expnass  11102  sqrt9  11835  ef01bndlem  12547  sin01bnd  12548  cos2bnd  12551  sin01gt0  12553  cos01gt0  12554  egt2lt3  12571  flodddiv4  12727  starvndxnmulrndx  13556  scandxnmulrndx  13568  vscandxnmulrndx  13573  ipndxnmulrndx  13586  tsetndxnmulrndx  13605  plendxnmulrndx  13619  dsndxnmulrndx  13634  slotsdifunifndx  13644  dveflem  15969  sincosq3sgn  16072  sincosq4sgn  16073  cosq23lt0  16077  coseq0q4123  16078  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos6thpi  16086  pigt3  16088  pige3  16089  cos02pilt1  16096  log2tlbndlog2  16237  log2ublog2  16241  ppiqub  16310  chtqub  16313  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgsdir2lem1  16369  2lgslem3  16442  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem4  16954  ex-fl  16961  ex-gcd  16967