Theorem 3re 9145

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 9131	. 2 ⊢ 3 = (2 + 1)
2		2re 9141	. . 3 ⊢ 2 ∈ ℝ
3		1re 8106	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8120	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2280	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2178  (class class class)co 5967  ℝcr 7959  1c1 7961   + caddc 7963  2c2 9122  3c3 9123

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203  df-2 9130  df-3 9131

This theorem is referenced by:  3cn  9146  4re  9148  3ne0  9166  3ap0  9167  4pos  9168  1lt3  9243  3lt4  9244  2lt4  9245  3lt5  9248  3lt6  9253  2lt6  9254  3lt7  9259  2lt7  9260  3lt8  9266  2lt8  9267  3lt9  9274  2lt9  9275  1le3  9283  8th4div3  9291  halfpm6th  9292  3halfnz  9505  3lt10  9675  2lt10  9676  uzuzle23  9727  uz3m2nn  9729  nn01to3  9773  3rp  9816  fz0to4untppr  10281  expnass  10827  sqrt9  11474  ef01bndlem  12182  sin01bnd  12183  cos2bnd  12186  sin01gt0  12188  cos01gt0  12189  egt2lt3  12206  flodddiv4  12362  starvndxnmulrndx  13091  scandxnmulrndx  13103  vscandxnmulrndx  13108  ipndxnmulrndx  13121  tsetndxnmulrndx  13140  plendxnmulrndx  13154  dsndxnmulrndx  13169  slotsdifunifndx  13179  dveflem  15313  sincosq3sgn  15415  sincosq4sgn  15416  cosq23lt0  15420  coseq0q4123  15421  coseq00topi  15422  coseq0negpitopi  15423  tangtx  15425  sincos6thpi  15429  pigt3  15431  pige3  15432  cos02pilt1  15438  lgsdir2lem1  15620  2lgslem3  15693  ex-fl  15861  ex-gcd  15867