Theorem 3re 12298

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 12281	. 2 ⊢ 3 = (2 + 1)
2		2re 12292	. . 3 ⊢ 2 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11197	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2858	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076  2c2 12272  3c3 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281

This theorem is referenced by:  4re  12302  2le3  12392  1lt3  12393  3lt4  12394  2lt4  12395  3lt5  12398  3lt6  12403  2lt6  12404  3lt7  12409  2lt7  12410  3lt8  12416  2lt8  12417  3lt9  12424  2lt9  12425  1le3  12432  3halfnz  12652  3lt10  12831  5eluz3  12884  uzuzle23  12885  uzuzle34  12887  uz3m2nn  12895  nn01to3  12942  3rp  12999  fz0to4untppr  13635  fz0to5un2tp  13636  expnass  14221  hashtpg  14498  hash3tpde  14506  01sqrexlem7  15275  sqrt9  15300  caucvgrlem  15700  bpoly4  16089  ef01bndlem  16216  sin01bnd  16217  cos2bnd  16220  sin01gt0  16222  cos01gt0  16223  egt2lt3  16238  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  flodddiv4  16449  ge2nprmge4  16736  starvndxnmulrndx  17335  scandxnmulrndx  17347  vscandxnmulrndx  17352  ipndxnmulrndx  17363  tsetndxnmulrndx  17387  plendxnmulrndx  17401  dsndxnmulrndx  17420  slotsdifunifndx  17430  vitalilem4  25673  dveflem  26041  sincosq3sgn  26565  sincosq4sgn  26566  tangtx  26570  sincos6thpi  26581  pigt3  26583  pige3  26584  pige3ALT  26585  ang180lem2  26875  1cubrlem  26906  log2cnv  27009  log2tlbnd  27010  log2ub  27014  cxploglim2  27043  basellem5  27149  basellem9  27153  ppiublem1  27266  ppiub  27268  chtub  27276  bposlem2  27349  bposlem3  27350  bposlem4  27351  bposlem5  27352  bposlem6  27353  bposlem8  27355  bposlem9  27356  lgsdir2lem1  27389  2lgslem3  27468  chebbnd1lem2  27534  chebbnd1lem3  27535  chebbnd1  27536  chto1ub  27540  dchrvmasumlem2  27562  dchrvmasumlema  27564  dchrvmasumiflem1  27565  mulog2sumlem2  27599  pntibndlem1  27653  pntibndlem2  27655  pntlemb  27661  pntlemk  27670  pntlemo  27671  istrkg3ld  28630  tgcgr4  28700  axlowdimlem16  29158  axlowdimlem17  29159  axlowdim  29162  usgrexmplef  29460  upgr4cycl4dv4e  30387  konigsbergiedgw  30450  konigsberglem1  30454  konigsberglem2  30455  konigsberglem3  30456  konigsberglem4  30457  frgrogt3nreg  30599  friendshipgt3  30600  friendship  30601  ex-dif  30625  ex-in  30627  ex-fl  30649  ex-ceil  30650  ex-gcd  30659  threehalves  33092  iconstr  34063  2sqr3minply  34077  cos9thpiminplylem3  34081  cos9thpinconstrlem1  34086  prodfzo03  34897  hgt750lem  34945  hgt750lem2  34946  hgt750leme  34952  cusgracyclt3v  35506  problem3  36017  problem5  36019  poimirlem9  38128  itg2addnclem2  38171  heiborlem5  38314  heiborlem6  38315  heiborlem7  38316  heiborlem8  38317  3lexlogpow5ineq2  42672  3lexlogpow5ineq4  42673  3lexlogpow5ineq3  42674  3lexlogpow2ineq1  42675  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1lem1  42679  aks4d1p1p3  42686  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p1p6  42690  aks4d1p1p5  42692  aks4d1p1  42693  aks4d1p2  42694  aks4d1p3  42695  aks4d1p5  42697  aks4d1p6  42698  aks4d1p7d1  42699  aks4d1p7  42700  aks4d1p8  42704  aks4d1p9  42705  2np3bcnp1  42761  2ap1caineq  42762  aks6d1c7lem1  42797  aks6d1c7lem2  42798  aks6d1c7  42801  aks5lem6  42809  aks5lem8  42818  acos1half  42967  sn-0ne2  43015  3cubeslem2  43266  3cubeslem4  43270  jm2.23  43573  lt4addmuld  45885  stoweidlem11  46585  stoweidlem13  46587  stoweidlem26  46600  stoweidlem34  46608  stoweidlem42  46616  stoweidlem59  46633  stoweidlem62  46636  stoweid  46637  wallispilem4  46642  fourierdlem87  46767  smfmullem4  47368  modm2nep1  47966  modm1nep2  47968  fmtnoge3  48139  fmtnoprmfac2lem1  48175  31prm  48206  9fppr8  48359  fpprel2  48363  nfermltl8rev  48364  nfermltl2rev  48365  gbegt5  48383  gboge9  48386  sbgoldbwt  48399  sbgoldbst  48400  sbgoldbalt  48403  sbgoldbo  48409  nnsum3primes4  48410  nnsum4primes4  48411  nnsum4primesprm  48413  nnsum3primesgbe  48414  nnsum4primesgbe  48415  nnsum3primesle9  48416  nnsum4primesle9  48417  evengpop3  48420  evengpoap3  48421  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  cycl3grtri  48569  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb3  48656  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659  gpgusgralem  48678  gpg3nbgrvtx0  48698  gpg3kgrtriexlem1  48705  gpg3kgrtriexlem3  48707  gpg3kgrtriexlem4  48708  gpg3kgrtriexlem6  48710  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgrpgt2nabl  48988  ackval42  49318  sepfsepc  49549