Theorem 3re 12261

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 12245	. 2 ⊢ 3 = (2 + 1)
2		2re 12255	. . 3 ⊢ 2 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  2c2 12236  3c3 12237

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245

This theorem is referenced by:  4re  12265  4pos  12288  1lt3  12349  3lt4  12350  2lt4  12351  3lt5  12354  3lt6  12359  2lt6  12360  3lt7  12365  2lt7  12366  3lt8  12372  2lt8  12373  3lt9  12380  2lt9  12381  1le3  12388  3halfnz  12608  3lt10  12781  2lt10  12782  5eluz3  12833  uzuzle23  12834  uzuzle34  12836  uz3m2nn  12844  nn01to3  12891  3rp  12948  fz0to4untppr  13584  fz0to5un2tp  13585  expnass  14170  hashtpg  14447  hash3tpde  14455  01sqrexlem7  15210  sqrt9  15235  caucvgrlem  15635  bpoly4  16024  ef01bndlem  16151  sin01bnd  16152  cos2bnd  16155  sin01gt0  16157  cos01gt0  16158  egt2lt3  16173  rpnnen2lem3  16183  rpnnen2lem4  16184  rpnnen2lem9  16189  flodddiv4  16384  ge2nprmge4  16671  starvndxnmulrndx  17269  scandxnmulrndx  17281  vscandxnmulrndx  17286  ipndxnmulrndx  17297  tsetndxnmulrndx  17321  plendxnmulrndx  17335  dsndxnmulrndx  17354  slotsdifunifndx  17364  vitalilem4  25578  dveflem  25946  sincosq3sgn  26464  sincosq4sgn  26465  tangtx  26469  sincos6thpi  26480  pigt3  26482  pige3  26483  pige3ALT  26484  ang180lem2  26774  1cubrlem  26805  log2cnv  26908  log2tlbnd  26909  log2ub  26913  cxploglim2  26942  basellem5  27048  basellem9  27052  ppiublem1  27165  ppiub  27167  chtub  27175  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  2lgslem3  27367  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chto1ub  27439  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  mulog2sumlem2  27498  pntibndlem1  27552  pntibndlem2  27554  pntlemb  27560  pntlemk  27569  pntlemo  27570  istrkg3ld  28529  tgcgr4  28599  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  usgrexmplef  29328  upgr4cycl4dv4e  30255  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberglem4  30325  frgrogt3nreg  30467  friendshipgt3  30468  friendship  30469  ex-dif  30493  ex-in  30495  ex-fl  30517  ex-ceil  30518  ex-gcd  30527  threehalves  32974  iconstr  33910  2sqr3minply  33924  cos9thpiminplylem3  33928  cos9thpinconstrlem1  33933  prodfzo03  34747  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  cusgracyclt3v  35338  problem3  35849  problem5  35851  poimirlem9  37950  itg2addnclem2  37993  heiborlem5  38136  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  2np3bcnp1  42583  2ap1caineq  42584  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  aks5lem8  42640  acos1half  42790  sn-0ne2  42838  3cubeslem2  43117  3cubeslem4  43121  jm2.23  43424  jm2.20nn  43425  lt4addmuld  45739  stoweidlem11  46439  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  stoweidlem42  46470  stoweidlem59  46487  stoweidlem62  46490  stoweid  46491  wallispilem4  46496  fourierdlem87  46621  smfmullem4  47222  modm2nep1  47820  modm1nep2  47822  fmtnoge3  47993  fmtnoprmfac2lem1  48029  31prm  48060  9fppr8  48213  fpprel2  48217  nfermltl8rev  48218  nfermltl2rev  48219  gbegt5  48237  gboge9  48240  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbalt  48257  sbgoldbo  48263  nnsum3primes4  48264  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum3primesgbe  48268  nnsum4primesgbe  48269  nnsum3primesle9  48270  nnsum4primesle9  48271  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  cycl3grtri  48423  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgusgralem  48532  gpg3nbgrvtx0  48552  gpg3kgrtriexlem1  48559  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgrpgt2nabl  48842  ackval42  49172  sepfsepc  49403