Theorem 3re 12154

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 12138	. 2 ⊢ 3 = (2 + 1)
2		2re 12148	. . 3 ⊢ 2 ∈ ℝ
3		1re 11076	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11091	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7337  ℝcr 10971  1c1 10973   + caddc 10975  2c2 12129  3c3 12130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-i2m1 11040  ax-1ne0 11041  ax-rrecex 11044  ax-cnre 11045

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-iota 6431  df-fv 6487  df-ov 7340  df-2 12137  df-3 12138

This theorem is referenced by:  4re  12158  3ne0  12180  4pos  12181  1lt3  12247  3lt4  12248  2lt4  12249  3lt5  12252  3lt6  12257  2lt6  12258  3lt7  12263  2lt7  12264  3lt8  12270  2lt8  12271  3lt9  12278  2lt9  12279  1le3  12286  3halfnz  12500  3lt10  12675  2lt10  12676  uzuzle23  12730  uz3m2nn  12732  nn01to3  12782  3rp  12837  fz0to4untppr  13460  expnass  14025  hashtpg  14299  sqrlem7  15059  sqrt9  15084  caucvgrlem  15483  bpoly4  15868  ef01bndlem  15992  sin01bnd  15993  cos2bnd  15996  sin01gt0  15998  cos01gt0  15999  egt2lt3  16014  rpnnen2lem3  16024  rpnnen2lem4  16025  rpnnen2lem9  16030  flodddiv4  16221  ge2nprmge4  16503  starvndxnmulrndx  17113  scandxnmulrndx  17125  vscandxnmulrndx  17130  ipndxnmulrndx  17141  tsetndxnmulrndx  17165  plendxnmulrndx  17179  dsndxnmulrndx  17198  slotsdifunifndx  17208  cnfldfunALTOLD  20717  matscaOLD  21669  matvscaOLD  21671  vitalilem4  24881  dveflem  25249  sincosq3sgn  25763  sincosq4sgn  25764  tangtx  25768  sincos6thpi  25778  pigt3  25780  pige3  25781  pige3ALT  25782  ang180lem2  26066  1cubrlem  26097  log2cnv  26200  log2tlbnd  26201  log2ub  26205  cxploglim2  26234  basellem5  26340  basellem9  26344  ppiublem1  26456  ppiub  26458  chtub  26466  bposlem2  26539  bposlem3  26540  bposlem4  26541  bposlem5  26542  bposlem6  26543  bposlem8  26545  bposlem9  26546  lgsdir2lem1  26579  2lgslem3  26658  chebbnd1lem2  26724  chebbnd1lem3  26725  chebbnd1  26726  chto1ub  26730  dchrvmasumlem2  26752  dchrvmasumlema  26754  dchrvmasumiflem1  26755  mulog2sumlem2  26789  pntibndlem1  26843  pntibndlem2  26845  pntlemb  26851  pntlemk  26860  pntlemo  26861  istrkg3ld  27111  tgcgr4  27181  axlowdimlem16  27614  axlowdimlem17  27615  axlowdim  27618  usgrexmplef  27915  upgr4cycl4dv4e  28837  konigsbergiedgw  28900  konigsberglem1  28904  konigsberglem2  28905  konigsberglem3  28906  konigsberglem4  28907  frgrogt3nreg  29049  friendshipgt3  29050  friendship  29051  ex-dif  29075  ex-in  29077  ex-fl  29099  ex-ceil  29100  ex-gcd  29109  threehalves  31476  resvmulrOLD  31835  prodfzo03  32883  hgt750lem  32931  hgt750lem2  32932  hgt750leme  32938  cusgracyclt3v  33417  problem3  33924  problem5  33926  poimirlem9  35899  itg2addnclem2  35942  heiborlem5  36086  heiborlem6  36087  heiborlem7  36088  heiborlem8  36089  3lexlogpow5ineq2  40325  3lexlogpow5ineq4  40326  3lexlogpow5ineq3  40327  3lexlogpow2ineq1  40328  3lexlogpow2ineq2  40329  3lexlogpow5ineq5  40330  aks4d1lem1  40332  aks4d1p1p3  40339  aks4d1p1p2  40340  aks4d1p1p4  40341  aks4d1p1p6  40343  aks4d1p1p5  40345  aks4d1p1  40346  aks4d1p2  40347  aks4d1p3  40348  aks4d1p5  40350  aks4d1p6  40351  aks4d1p7d1  40352  aks4d1p7  40353  aks4d1p8  40357  aks4d1p9  40358  2np3bcnp1  40365  2ap1caineq  40366  2xp3dxp2ge1d  40427  acos1half  40435  sn-0ne2  40657  3cubeslem2  40777  3cubeslem4  40781  jm2.23  41089  jm2.20nn  41090  mnringscadOLD  42171  mnringvscadOLD  42173  lt4addmuld  43189  stoweidlem11  43897  stoweidlem13  43899  stoweidlem26  43912  stoweidlem34  43920  stoweidlem42  43928  stoweidlem59  43945  stoweidlem62  43948  stoweid  43949  wallispilem4  43954  fourierdlem87  44079  smfmullem4  44678  fmtnoge3  45342  fmtnoprmfac2lem1  45378  31prm  45409  9fppr8  45549  fpprel2  45553  nfermltl8rev  45554  nfermltl2rev  45555  gbegt5  45573  gboge9  45576  sbgoldbwt  45589  sbgoldbst  45590  sbgoldbalt  45593  sbgoldbo  45599  nnsum3primes4  45600  nnsum4primes4  45601  nnsum4primesprm  45603  nnsum3primesgbe  45604  nnsum4primesgbe  45605  nnsum3primesle9  45606  nnsum4primesle9  45607  evengpop3  45610  evengpoap3  45611  nnsum4primeseven  45612  nnsum4primesevenALTV  45613  wtgoldbnnsum4prm  45614  bgoldbnnsum3prm  45616  pgrpgt2nabl  46062  ackval42  46402  sepfsepc  46581