Theorem 3re 12252

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 12236	. 2 ⊢ 3 = (2 + 1)
2		2re 12246	. . 3 ⊢ 2 ∈ ℝ
3		1re 11135	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11151	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028  1c1 11030   + caddc 11032  2c2 12227  3c3 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235  df-3 12236

This theorem is referenced by:  4re  12256  4pos  12279  1lt3  12340  3lt4  12341  2lt4  12342  3lt5  12345  3lt6  12350  2lt6  12351  3lt7  12356  2lt7  12357  3lt8  12363  2lt8  12364  3lt9  12371  2lt9  12372  1le3  12379  3halfnz  12599  3lt10  12772  2lt10  12773  5eluz3  12824  uzuzle23  12825  uzuzle34  12827  uz3m2nn  12835  nn01to3  12882  3rp  12939  fz0to4untppr  13575  fz0to5un2tp  13576  expnass  14161  hashtpg  14438  hash3tpde  14446  01sqrexlem7  15201  sqrt9  15226  caucvgrlem  15626  bpoly4  16015  ef01bndlem  16142  sin01bnd  16143  cos2bnd  16146  sin01gt0  16148  cos01gt0  16149  egt2lt3  16164  rpnnen2lem3  16174  rpnnen2lem4  16175  rpnnen2lem9  16180  flodddiv4  16375  ge2nprmge4  16662  starvndxnmulrndx  17260  scandxnmulrndx  17272  vscandxnmulrndx  17277  ipndxnmulrndx  17288  tsetndxnmulrndx  17312  plendxnmulrndx  17326  dsndxnmulrndx  17345  slotsdifunifndx  17355  vitalilem4  25596  dveflem  25964  sincosq3sgn  26482  sincosq4sgn  26483  tangtx  26487  sincos6thpi  26498  pigt3  26500  pige3  26501  pige3ALT  26502  ang180lem2  26792  1cubrlem  26823  log2cnv  26926  log2tlbnd  26927  log2ub  26931  cxploglim2  26960  basellem5  27066  basellem9  27070  ppiublem1  27183  ppiub  27185  chtub  27193  bposlem2  27266  bposlem3  27267  bposlem4  27268  bposlem5  27269  bposlem6  27270  bposlem8  27272  bposlem9  27273  lgsdir2lem1  27306  2lgslem3  27385  chebbnd1lem2  27451  chebbnd1lem3  27452  chebbnd1  27453  chto1ub  27457  dchrvmasumlem2  27479  dchrvmasumlema  27481  dchrvmasumiflem1  27482  mulog2sumlem2  27516  pntibndlem1  27570  pntibndlem2  27572  pntlemb  27578  pntlemk  27587  pntlemo  27588  istrkg3ld  28547  tgcgr4  28617  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  usgrexmplef  29346  upgr4cycl4dv4e  30273  konigsbergiedgw  30336  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  konigsberglem4  30343  frgrogt3nreg  30485  friendshipgt3  30486  friendship  30487  ex-dif  30511  ex-in  30513  ex-fl  30535  ex-ceil  30536  ex-gcd  30545  threehalves  32993  iconstr  33950  2sqr3minply  33964  cos9thpiminplylem3  33968  cos9thpinconstrlem1  33973  prodfzo03  34787  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  cusgracyclt3v  35384  problem3  35895  problem5  35897  poimirlem9  37996  itg2addnclem2  38039  heiborlem5  38182  heiborlem6  38183  heiborlem7  38184  heiborlem8  38185  3lexlogpow5ineq2  42540  3lexlogpow5ineq4  42541  3lexlogpow5ineq3  42542  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1lem1  42547  aks4d1p1p3  42554  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p2  42562  aks4d1p3  42563  aks4d1p5  42565  aks4d1p6  42566  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  2np3bcnp1  42629  2ap1caineq  42630  aks6d1c7lem1  42665  aks6d1c7lem2  42666  aks6d1c7  42669  aks5lem6  42677  aks5lem8  42686  acos1half  42835  sn-0ne2  42883  3cubeslem2  43134  3cubeslem4  43138  jm2.23  43441  jm2.20nn  43442  lt4addmuld  45754  stoweidlem11  46454  stoweidlem13  46456  stoweidlem26  46469  stoweidlem34  46477  stoweidlem42  46485  stoweidlem59  46502  stoweidlem62  46505  stoweid  46506  wallispilem4  46511  fourierdlem87  46636  smfmullem4  47237  modm2nep1  47835  modm1nep2  47837  fmtnoge3  48008  fmtnoprmfac2lem1  48044  31prm  48075  9fppr8  48228  fpprel2  48232  nfermltl8rev  48233  nfermltl2rev  48234  gbegt5  48252  gboge9  48255  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbalt  48272  sbgoldbo  48278  nnsum3primes4  48279  nnsum4primes4  48280  nnsum4primesprm  48282  nnsum3primesgbe  48283  nnsum4primesgbe  48284  nnsum3primesle9  48285  nnsum4primesle9  48286  evengpop3  48289  evengpoap3  48290  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  cycl3grtri  48438  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpgusgralem  48547  gpg3nbgrvtx0  48567  gpg3kgrtriexlem1  48574  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem4  48577  gpg3kgrtriexlem6  48579  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgrpgt2nabl  48857  ackval42  49187  sepfsepc  49418