Theorem 3re 12255

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 12239	. 2 ⊢ 3 = (2 + 1)
2		2re 12249	. . 3 ⊢ 2 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  2c2 12230  3c3 12231

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239

This theorem is referenced by:  4re  12259  4pos  12282  1lt3  12343  3lt4  12344  2lt4  12345  3lt5  12348  3lt6  12353  2lt6  12354  3lt7  12359  2lt7  12360  3lt8  12366  2lt8  12367  3lt9  12374  2lt9  12375  1le3  12382  3halfnz  12602  3lt10  12775  2lt10  12776  5eluz3  12827  uzuzle23  12828  uzuzle34  12830  uz3m2nn  12838  nn01to3  12885  3rp  12942  fz0to4untppr  13578  fz0to5un2tp  13579  expnass  14164  hashtpg  14441  hash3tpde  14449  01sqrexlem7  15204  sqrt9  15229  caucvgrlem  15629  bpoly4  16018  ef01bndlem  16145  sin01bnd  16146  cos2bnd  16149  sin01gt0  16151  cos01gt0  16152  egt2lt3  16167  rpnnen2lem3  16177  rpnnen2lem4  16178  rpnnen2lem9  16183  flodddiv4  16378  ge2nprmge4  16665  starvndxnmulrndx  17263  scandxnmulrndx  17275  vscandxnmulrndx  17280  ipndxnmulrndx  17291  tsetndxnmulrndx  17315  plendxnmulrndx  17329  dsndxnmulrndx  17348  slotsdifunifndx  17358  vitalilem4  25591  dveflem  25959  sincosq3sgn  26480  sincosq4sgn  26481  tangtx  26485  sincos6thpi  26496  pigt3  26498  pige3  26499  pige3ALT  26500  ang180lem2  26790  1cubrlem  26821  log2cnv  26924  log2tlbnd  26925  log2ub  26929  cxploglim2  26959  basellem5  27065  basellem9  27069  ppiublem1  27182  ppiub  27184  chtub  27192  bposlem2  27265  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  bposlem8  27271  bposlem9  27272  lgsdir2lem1  27305  2lgslem3  27384  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chto1ub  27456  dchrvmasumlem2  27478  dchrvmasumlema  27480  dchrvmasumiflem1  27481  mulog2sumlem2  27515  pntibndlem1  27569  pntibndlem2  27571  pntlemb  27577  pntlemk  27586  pntlemo  27587  istrkg3ld  28546  tgcgr4  28616  axlowdimlem16  29043  axlowdimlem17  29044  axlowdim  29047  usgrexmplef  29345  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  32992  iconstr  33929  2sqr3minply  33943  cos9thpiminplylem3  33947  cos9thpinconstrlem1  33952  prodfzo03  34766  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  cusgracyclt3v  35357  problem3  35868  problem5  35870  poimirlem9  37967  itg2addnclem2  38010  heiborlem5  38153  heiborlem6  38154  heiborlem7  38155  heiborlem8  38156  3lexlogpow5ineq2  42511  3lexlogpow5ineq4  42512  3lexlogpow5ineq3  42513  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1lem1  42518  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  aks4d1p9  42544  2np3bcnp1  42600  2ap1caineq  42601  aks6d1c7lem1  42636  aks6d1c7lem2  42637  aks6d1c7  42640  aks5lem6  42648  aks5lem8  42657  acos1half  42807  sn-0ne2  42855  3cubeslem2  43134  3cubeslem4  43138  jm2.23  43445  jm2.20nn  43446  lt4addmuld  45760  stoweidlem11  46460  stoweidlem13  46462  stoweidlem26  46475  stoweidlem34  46483  stoweidlem42  46491  stoweidlem59  46508  stoweidlem62  46511  stoweid  46512  wallispilem4  46517  fourierdlem87  46642  smfmullem4  47243  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