Theorem 3re 12291

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 12275	. 2 ⊢ 3 = (2 + 1)
2		2re 12285	. . 3 ⊢ 2 ∈ ℝ
3		1re 11213	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11228	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2829	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7408  ℝcr 11108  1c1 11110   + caddc 11112  2c2 12266  3c3 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-i2m1 11177  ax-1ne0 11178  ax-rrecex 11181  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411  df-2 12274  df-3 12275

This theorem is referenced by:  4re  12295  3ne0  12317  4pos  12318  1lt3  12384  3lt4  12385  2lt4  12386  3lt5  12389  3lt6  12394  2lt6  12395  3lt7  12400  2lt7  12401  3lt8  12407  2lt8  12408  3lt9  12415  2lt9  12416  1le3  12423  3halfnz  12640  3lt10  12813  2lt10  12814  uzuzle23  12872  uz3m2nn  12874  nn01to3  12924  3rp  12979  fz0to4untppr  13603  expnass  14171  hashtpg  14445  01sqrexlem7  15194  sqrt9  15219  caucvgrlem  15618  bpoly4  16002  ef01bndlem  16126  sin01bnd  16127  cos2bnd  16130  sin01gt0  16132  cos01gt0  16133  egt2lt3  16148  rpnnen2lem3  16158  rpnnen2lem4  16159  rpnnen2lem9  16164  flodddiv4  16355  ge2nprmge4  16637  starvndxnmulrndx  17250  scandxnmulrndx  17262  vscandxnmulrndx  17267  ipndxnmulrndx  17278  tsetndxnmulrndx  17302  plendxnmulrndx  17316  dsndxnmulrndx  17335  slotsdifunifndx  17345  cnfldfunALTOLD  20957  matscaOLD  21915  matvscaOLD  21917  vitalilem4  25127  dveflem  25495  sincosq3sgn  26009  sincosq4sgn  26010  tangtx  26014  sincos6thpi  26024  pigt3  26026  pige3  26027  pige3ALT  26028  ang180lem2  26312  1cubrlem  26343  log2cnv  26446  log2tlbnd  26447  log2ub  26451  cxploglim2  26480  basellem5  26586  basellem9  26590  ppiublem1  26702  ppiub  26704  chtub  26712  bposlem2  26785  bposlem3  26786  bposlem4  26787  bposlem5  26788  bposlem6  26789  bposlem8  26791  bposlem9  26792  lgsdir2lem1  26825  2lgslem3  26904  chebbnd1lem2  26970  chebbnd1lem3  26971  chebbnd1  26972  chto1ub  26976  dchrvmasumlem2  26998  dchrvmasumlema  27000  dchrvmasumiflem1  27001  mulog2sumlem2  27035  pntibndlem1  27089  pntibndlem2  27091  pntlemb  27097  pntlemk  27106  pntlemo  27107  istrkg3ld  27709  tgcgr4  27779  axlowdimlem16  28212  axlowdimlem17  28213  axlowdim  28216  usgrexmplef  28513  upgr4cycl4dv4e  29435  konigsbergiedgw  29498  konigsberglem1  29502  konigsberglem2  29503  konigsberglem3  29504  konigsberglem4  29505  frgrogt3nreg  29647  friendshipgt3  29648  friendship  29649  ex-dif  29673  ex-in  29675  ex-fl  29697  ex-ceil  29698  ex-gcd  29707  threehalves  32076  resvmulrOLD  32449  prodfzo03  33610  hgt750lem  33658  hgt750lem2  33659  hgt750leme  33665  cusgracyclt3v  34142  problem3  34647  problem5  34649  poimirlem9  36492  itg2addnclem2  36535  heiborlem5  36678  heiborlem6  36679  heiborlem7  36680  heiborlem8  36681  3lexlogpow5ineq2  40915  3lexlogpow5ineq4  40916  3lexlogpow5ineq3  40917  3lexlogpow2ineq1  40918  3lexlogpow2ineq2  40919  3lexlogpow5ineq5  40920  aks4d1lem1  40922  aks4d1p1p3  40929  aks4d1p1p2  40930  aks4d1p1p4  40931  aks4d1p1p6  40933  aks4d1p1p5  40935  aks4d1p1  40936  aks4d1p2  40937  aks4d1p3  40938  aks4d1p5  40940  aks4d1p6  40941  aks4d1p7d1  40942  aks4d1p7  40943  aks4d1p8  40947  aks4d1p9  40948  2np3bcnp1  40955  2ap1caineq  40956  2xp3dxp2ge1d  41017  acos1half  41025  sn-0ne2  41280  3cubeslem2  41413  3cubeslem4  41417  jm2.23  41725  jm2.20nn  41726  mnringscadOLD  42972  mnringvscadOLD  42974  lt4addmuld  44006  stoweidlem11  44717  stoweidlem13  44719  stoweidlem26  44732  stoweidlem34  44740  stoweidlem42  44748  stoweidlem59  44765  stoweidlem62  44768  stoweid  44769  wallispilem4  44774  fourierdlem87  44899  smfmullem4  45500  fmtnoge3  46188  fmtnoprmfac2lem1  46224  31prm  46255  9fppr8  46395  fpprel2  46399  nfermltl8rev  46400  nfermltl2rev  46401  gbegt5  46419  gboge9  46422  sbgoldbwt  46435  sbgoldbst  46436  sbgoldbalt  46439  sbgoldbo  46445  nnsum3primes4  46446  nnsum4primes4  46447  nnsum4primesprm  46449  nnsum3primesgbe  46450  nnsum4primesgbe  46451  nnsum3primesle9  46452  nnsum4primesle9  46453  evengpop3  46456  evengpoap3  46457  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  wtgoldbnnsum4prm  46460  bgoldbnnsum3prm  46462  pgrpgt2nabl  47032  ackval42  47372  sepfsepc  47550