Theorem 3re 12335

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 12319	. 2 ⊢ 3 = (2 + 1)
2		2re 12329	. . 3 ⊢ 2 ∈ ℝ
3		1re 11252	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11267	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2822	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2099  (class class class)co 7413  ℝcr 11145  1c1 11147   + caddc 11149  2c2 12310  3c3 12311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-i2m1 11214  ax-1ne0 11215  ax-rrecex 11218  ax-cnre 11219

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7416  df-2 12318  df-3 12319

This theorem is referenced by:  4re  12339  3ne0  12361  4pos  12362  1lt3  12428  3lt4  12429  2lt4  12430  3lt5  12433  3lt6  12438  2lt6  12439  3lt7  12444  2lt7  12445  3lt8  12451  2lt8  12452  3lt9  12459  2lt9  12460  1le3  12467  3halfnz  12684  3lt10  12857  2lt10  12858  uzuzle23  12916  uz3m2nn  12918  nn01to3  12968  3rp  13025  fz0to4untppr  13649  expnass  14217  hashtpg  14496  01sqrexlem7  15245  sqrt9  15270  caucvgrlem  15669  bpoly4  16053  ef01bndlem  16178  sin01bnd  16179  cos2bnd  16182  sin01gt0  16184  cos01gt0  16185  egt2lt3  16200  rpnnen2lem3  16210  rpnnen2lem4  16211  rpnnen2lem9  16216  flodddiv4  16407  ge2nprmge4  16694  starvndxnmulrndx  17312  scandxnmulrndx  17324  vscandxnmulrndx  17329  ipndxnmulrndx  17340  tsetndxnmulrndx  17364  plendxnmulrndx  17378  dsndxnmulrndx  17397  slotsdifunifndx  17407  cnfldfunALTOLDOLD  21365  matscaOLD  22401  matvscaOLD  22403  vitalilem4  25625  dveflem  25996  sincosq3sgn  26522  sincosq4sgn  26523  tangtx  26527  sincos6thpi  26537  pigt3  26539  pige3  26540  pige3ALT  26541  ang180lem2  26832  1cubrlem  26863  log2cnv  26966  log2tlbnd  26967  log2ub  26971  cxploglim2  27001  basellem5  27107  basellem9  27111  ppiublem1  27225  ppiub  27227  chtub  27235  bposlem2  27308  bposlem3  27309  bposlem4  27310  bposlem5  27311  bposlem6  27312  bposlem8  27314  bposlem9  27315  lgsdir2lem1  27348  2lgslem3  27427  chebbnd1lem2  27493  chebbnd1lem3  27494  chebbnd1  27495  chto1ub  27499  dchrvmasumlem2  27521  dchrvmasumlema  27523  dchrvmasumiflem1  27524  mulog2sumlem2  27558  pntibndlem1  27612  pntibndlem2  27614  pntlemb  27620  pntlemk  27629  pntlemo  27630  istrkg3ld  28382  tgcgr4  28452  axlowdimlem16  28885  axlowdimlem17  28886  axlowdim  28889  usgrexmplef  29189  upgr4cycl4dv4e  30112  konigsbergiedgw  30175  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  konigsberglem4  30182  frgrogt3nreg  30324  friendshipgt3  30325  friendship  30326  ex-dif  30350  ex-in  30352  ex-fl  30374  ex-ceil  30375  ex-gcd  30384  threehalves  32776  resvmulrOLD  33216  2sqr3minply  33617  prodfzo03  34459  hgt750lem  34507  hgt750lem2  34508  hgt750leme  34514  cusgracyclt3v  34994  problem3  35505  problem5  35507  poimirlem9  37340  itg2addnclem2  37383  heiborlem5  37526  heiborlem6  37527  heiborlem7  37528  heiborlem8  37529  3lexlogpow5ineq2  41764  3lexlogpow5ineq4  41765  3lexlogpow5ineq3  41766  3lexlogpow2ineq1  41767  3lexlogpow2ineq2  41768  3lexlogpow5ineq5  41769  aks4d1lem1  41771  aks4d1p1p3  41778  aks4d1p1p2  41779  aks4d1p1p4  41780  aks4d1p1p6  41782  aks4d1p1p5  41784  aks4d1p1  41785  aks4d1p2  41786  aks4d1p3  41787  aks4d1p5  41789  aks4d1p6  41790  aks4d1p7d1  41791  aks4d1p7  41792  aks4d1p8  41796  aks4d1p9  41797  2np3bcnp1  41853  2ap1caineq  41854  aks6d1c7lem1  41889  aks6d1c7lem2  41890  aks6d1c7  41893  aks5lem6  41901  2xp3dxp2ge1d  41946  sn-0ne2  42114  acos1half  42363  3cubeslem2  42376  3cubeslem4  42380  jm2.23  42688  jm2.20nn  42689  mnringscadOLD  43931  mnringvscadOLD  43933  lt4addmuld  44954  stoweidlem11  45665  stoweidlem13  45667  stoweidlem26  45680  stoweidlem34  45688  stoweidlem42  45696  stoweidlem59  45713  stoweidlem62  45716  stoweid  45717  wallispilem4  45722  fourierdlem87  45847  smfmullem4  46448  fmtnoge3  47135  fmtnoprmfac2lem1  47171  31prm  47202  9fppr8  47342  fpprel2  47346  nfermltl8rev  47347  nfermltl2rev  47348  gbegt5  47366  gboge9  47369  sbgoldbwt  47382  sbgoldbst  47383  sbgoldbalt  47386  sbgoldbo  47392  nnsum3primes4  47393  nnsum4primes4  47394  nnsum4primesprm  47396  nnsum3primesgbe  47397  nnsum4primesgbe  47398  nnsum3primesle9  47399  nnsum4primesle9  47400  evengpop3  47403  evengpoap3  47404  nnsum4primeseven  47405  nnsum4primesevenALTV  47406  wtgoldbnnsum4prm  47407  bgoldbnnsum3prm  47409  pgrpgt2nabl  47778  ackval42  48117  sepfsepc  48294