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 12282	. 2 ⊢ 3 = (2 + 1)
2		2re 12292	. . 3 ⊢ 2 ∈ ℝ
3		1re 11220	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11235	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2104  (class class class)co 7413  ℝcr 11113  1c1 11115   + caddc 11117  2c2 12273  3c3 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7416  df-2 12281  df-3 12282

This theorem is referenced by:  4re  12302  3ne0  12324  4pos  12325  1lt3  12391  3lt4  12392  2lt4  12393  3lt5  12396  3lt6  12401  2lt6  12402  3lt7  12407  2lt7  12408  3lt8  12414  2lt8  12415  3lt9  12422  2lt9  12423  1le3  12430  3halfnz  12647  3lt10  12820  2lt10  12821  uzuzle23  12879  uz3m2nn  12881  nn01to3  12931  3rp  12986  fz0to4untppr  13610  expnass  14178  hashtpg  14452  01sqrexlem7  15201  sqrt9  15226  caucvgrlem  15625  bpoly4  16009  ef01bndlem  16133  sin01bnd  16134  cos2bnd  16137  sin01gt0  16139  cos01gt0  16140  egt2lt3  16155  rpnnen2lem3  16165  rpnnen2lem4  16166  rpnnen2lem9  16171  flodddiv4  16362  ge2nprmge4  16644  starvndxnmulrndx  17257  scandxnmulrndx  17269  vscandxnmulrndx  17274  ipndxnmulrndx  17285  tsetndxnmulrndx  17309  plendxnmulrndx  17323  dsndxnmulrndx  17342  slotsdifunifndx  17352  cnfldfunALTOLD  21160  matscaOLD  22138  matvscaOLD  22140  vitalilem4  25362  dveflem  25730  sincosq3sgn  26244  sincosq4sgn  26245  tangtx  26249  sincos6thpi  26259  pigt3  26261  pige3  26262  pige3ALT  26263  ang180lem2  26549  1cubrlem  26580  log2cnv  26683  log2tlbnd  26684  log2ub  26688  cxploglim2  26717  basellem5  26823  basellem9  26827  ppiublem1  26939  ppiub  26941  chtub  26949  bposlem2  27022  bposlem3  27023  bposlem4  27024  bposlem5  27025  bposlem6  27026  bposlem8  27028  bposlem9  27029  lgsdir2lem1  27062  2lgslem3  27141  chebbnd1lem2  27207  chebbnd1lem3  27208  chebbnd1  27209  chto1ub  27213  dchrvmasumlem2  27235  dchrvmasumlema  27237  dchrvmasumiflem1  27238  mulog2sumlem2  27272  pntibndlem1  27326  pntibndlem2  27328  pntlemb  27334  pntlemk  27343  pntlemo  27344  istrkg3ld  27977  tgcgr4  28047  axlowdimlem16  28480  axlowdimlem17  28481  axlowdim  28484  usgrexmplef  28781  upgr4cycl4dv4e  29703  konigsbergiedgw  29766  konigsberglem1  29770  konigsberglem2  29771  konigsberglem3  29772  konigsberglem4  29773  frgrogt3nreg  29915  friendshipgt3  29916  friendship  29917  ex-dif  29941  ex-in  29943  ex-fl  29965  ex-ceil  29966  ex-gcd  29975  threehalves  32346  resvmulrOLD  32722  prodfzo03  33911  hgt750lem  33959  hgt750lem2  33960  hgt750leme  33966  cusgracyclt3v  34443  problem3  34948  problem5  34950  poimirlem9  36802  itg2addnclem2  36845  heiborlem5  36988  heiborlem6  36989  heiborlem7  36990  heiborlem8  36991  3lexlogpow5ineq2  41228  3lexlogpow5ineq4  41229  3lexlogpow5ineq3  41230  3lexlogpow2ineq1  41231  3lexlogpow2ineq2  41232  3lexlogpow5ineq5  41233  aks4d1lem1  41235  aks4d1p1p3  41242  aks4d1p1p2  41243  aks4d1p1p4  41244  aks4d1p1p6  41246  aks4d1p1p5  41248  aks4d1p1  41249  aks4d1p2  41250  aks4d1p3  41251  aks4d1p5  41253  aks4d1p6  41254  aks4d1p7d1  41255  aks4d1p7  41256  aks4d1p8  41260  aks4d1p9  41261  2np3bcnp1  41268  2ap1caineq  41269  2xp3dxp2ge1d  41330  sn-0ne2  41583  acos1half  41719  3cubeslem2  41727  3cubeslem4  41731  jm2.23  42039  jm2.20nn  42040  mnringscadOLD  43286  mnringvscadOLD  43288  lt4addmuld  44316  stoweidlem11  45027  stoweidlem13  45029  stoweidlem26  45042  stoweidlem34  45050  stoweidlem42  45058  stoweidlem59  45075  stoweidlem62  45078  stoweid  45079  wallispilem4  45084  fourierdlem87  45209  smfmullem4  45810  fmtnoge3  46498  fmtnoprmfac2lem1  46534  31prm  46565  9fppr8  46705  fpprel2  46709  nfermltl8rev  46710  nfermltl2rev  46711  gbegt5  46729  gboge9  46732  sbgoldbwt  46745  sbgoldbst  46746  sbgoldbalt  46749  sbgoldbo  46755  nnsum3primes4  46756  nnsum4primes4  46757  nnsum4primesprm  46759  nnsum3primesgbe  46760  nnsum4primesgbe  46761  nnsum3primesle9  46762  nnsum4primesle9  46763  evengpop3  46766  evengpoap3  46767  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  wtgoldbnnsum4prm  46770  bgoldbnnsum3prm  46772  pgrpgt2nabl  47132  ackval42  47471  sepfsepc  47649