Theorem 3re 12237

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 12221	. 2 ⊢ 3 = (2 + 1)
2		2re 12231	. . 3 ⊢ 2 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11159	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041  2c2 12212  3c3 12213

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 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221

This theorem is referenced by:  4re  12241  4pos  12264  1lt3  12325  3lt4  12326  2lt4  12327  3lt5  12330  3lt6  12335  2lt6  12336  3lt7  12341  2lt7  12342  3lt8  12348  2lt8  12349  3lt9  12356  2lt9  12357  1le3  12364  3halfnz  12583  3lt10  12756  2lt10  12757  5eluz3  12808  uzuzle23  12809  uzuzle34  12811  uz3m2nn  12819  nn01to3  12866  3rp  12923  fz0to4untppr  13558  fz0to5un2tp  13559  expnass  14143  hashtpg  14420  hash3tpde  14428  01sqrexlem7  15183  sqrt9  15208  caucvgrlem  15608  bpoly4  15994  ef01bndlem  16121  sin01bnd  16122  cos2bnd  16125  sin01gt0  16127  cos01gt0  16128  egt2lt3  16143  rpnnen2lem3  16153  rpnnen2lem4  16154  rpnnen2lem9  16159  flodddiv4  16354  ge2nprmge4  16640  starvndxnmulrndx  17238  scandxnmulrndx  17250  vscandxnmulrndx  17255  ipndxnmulrndx  17266  tsetndxnmulrndx  17290  plendxnmulrndx  17304  dsndxnmulrndx  17323  slotsdifunifndx  17333  vitalilem4  25583  dveflem  25954  sincosq3sgn  26480  sincosq4sgn  26481  tangtx  26485  sincos6thpi  26496  pigt3  26498  pige3  26499  pige3ALT  26500  ang180lem2  26791  1cubrlem  26822  log2cnv  26925  log2tlbnd  26926  log2ub  26930  cxploglim2  26960  basellem5  27066  basellem9  27070  ppiublem1  27184  ppiub  27186  chtub  27194  bposlem2  27267  bposlem3  27268  bposlem4  27269  bposlem5  27270  bposlem6  27271  bposlem8  27273  bposlem9  27274  lgsdir2lem1  27307  2lgslem3  27386  chebbnd1lem2  27452  chebbnd1lem3  27453  chebbnd1  27454  chto1ub  27458  dchrvmasumlem2  27480  dchrvmasumlema  27482  dchrvmasumiflem1  27483  mulog2sumlem2  27517  pntibndlem1  27571  pntibndlem2  27573  pntlemb  27579  pntlemk  27588  pntlemo  27589  istrkg3ld  28549  tgcgr4  28619  axlowdimlem16  29046  axlowdimlem17  29047  axlowdim  29050  usgrexmplef  29348  upgr4cycl4dv4e  30276  konigsbergiedgw  30339  konigsberglem1  30343  konigsberglem2  30344  konigsberglem3  30345  konigsberglem4  30346  frgrogt3nreg  30488  friendshipgt3  30489  friendship  30490  ex-dif  30514  ex-in  30516  ex-fl  30538  ex-ceil  30539  ex-gcd  30548  threehalves  33011  iconstr  33948  2sqr3minply  33962  cos9thpiminplylem3  33966  cos9thpinconstrlem1  33971  prodfzo03  34785  hgt750lem  34833  hgt750lem2  34834  hgt750leme  34840  cusgracyclt3v  35376  problem3  35887  problem5  35889  poimirlem9  37884  itg2addnclem2  37927  heiborlem5  38070  heiborlem6  38071  heiborlem7  38072  heiborlem8  38073  3lexlogpow5ineq2  42429  3lexlogpow5ineq4  42430  3lexlogpow5ineq3  42431  3lexlogpow2ineq1  42432  3lexlogpow2ineq2  42433  3lexlogpow5ineq5  42434  aks4d1lem1  42436  aks4d1p1p3  42443  aks4d1p1p2  42444  aks4d1p1p4  42445  aks4d1p1p6  42447  aks4d1p1p5  42449  aks4d1p1  42450  aks4d1p2  42451  aks4d1p3  42452  aks4d1p5  42454  aks4d1p6  42455  aks4d1p7d1  42456  aks4d1p7  42457  aks4d1p8  42461  aks4d1p9  42462  2np3bcnp1  42518  2ap1caineq  42519  aks6d1c7lem1  42554  aks6d1c7lem2  42555  aks6d1c7  42558  aks5lem6  42566  aks5lem8  42575  acos1half  42732  sn-0ne2  42780  3cubeslem2  43046  3cubeslem4  43050  jm2.23  43357  jm2.20nn  43358  lt4addmuld  45672  stoweidlem11  46373  stoweidlem13  46375  stoweidlem26  46388  stoweidlem34  46396  stoweidlem42  46404  stoweidlem59  46421  stoweidlem62  46424  stoweid  46425  wallispilem4  46430  fourierdlem87  46555  smfmullem4  47156  modm2nep1  47730  modm1nep2  47732  fmtnoge3  47894  fmtnoprmfac2lem1  47930  31prm  47961  9fppr8  48101  fpprel2  48105  nfermltl8rev  48106  nfermltl2rev  48107  gbegt5  48125  gboge9  48128  sbgoldbwt  48141  sbgoldbst  48142  sbgoldbalt  48145  sbgoldbo  48151  nnsum3primes4  48152  nnsum4primes4  48153  nnsum4primesprm  48155  nnsum3primesgbe  48156  nnsum4primesgbe  48157  nnsum3primesle9  48158  nnsum4primesle9  48159  evengpop3  48162  evengpoap3  48163  nnsum4primeseven  48164  nnsum4primesevenALTV  48165  wtgoldbnnsum4prm  48166  bgoldbnnsum3prm  48168  cycl3grtri  48311  usgrexmpl1lem  48385  usgrexmpl2lem  48390  usgrexmpl2nb3  48398  usgrexmpl2nb4  48399  usgrexmpl2nb5  48400  usgrexmpl2trifr  48401  gpgusgralem  48420  gpg3nbgrvtx0  48440  gpg3kgrtriexlem1  48447  gpg3kgrtriexlem3  48449  gpg3kgrtriexlem4  48450  gpg3kgrtriexlem6  48452  pgnbgreunbgrlem2lem1  48478  pgnbgreunbgrlem2lem2  48479  pgrpgt2nabl  48730  ackval42  49060  sepfsepc  49291