Theorem 3re 12197

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 12181	. 2 ⊢ 3 = (2 + 1)
2		2re 12191	. . 3 ⊢ 2 ∈ ℝ
3		1re 11104	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11119	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2110  (class class class)co 7341  ℝcr 10997  1c1 10999   + caddc 11001  2c2 12172  3c3 12173

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 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-i2m1 11066  ax-1ne0 11067  ax-rrecex 11070  ax-cnre 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344  df-2 12180  df-3 12181

This theorem is referenced by:  4re  12201  4pos  12224  1lt3  12285  3lt4  12286  2lt4  12287  3lt5  12290  3lt6  12295  2lt6  12296  3lt7  12301  2lt7  12302  3lt8  12308  2lt8  12309  3lt9  12316  2lt9  12317  1le3  12324  3halfnz  12544  3lt10  12717  2lt10  12718  5eluz3  12773  uzuzle23  12774  uzuzle34  12776  uz3m2nn  12784  nn01to3  12831  3rp  12888  fz0to4untppr  13522  fz0to5un2tp  13523  expnass  14107  hashtpg  14384  hash3tpde  14392  01sqrexlem7  15147  sqrt9  15172  caucvgrlem  15572  bpoly4  15958  ef01bndlem  16085  sin01bnd  16086  cos2bnd  16089  sin01gt0  16091  cos01gt0  16092  egt2lt3  16107  rpnnen2lem3  16117  rpnnen2lem4  16118  rpnnen2lem9  16123  flodddiv4  16318  ge2nprmge4  16604  starvndxnmulrndx  17202  scandxnmulrndx  17214  vscandxnmulrndx  17219  ipndxnmulrndx  17230  tsetndxnmulrndx  17254  plendxnmulrndx  17268  dsndxnmulrndx  17287  slotsdifunifndx  17297  vitalilem4  25532  dveflem  25903  sincosq3sgn  26429  sincosq4sgn  26430  tangtx  26434  sincos6thpi  26445  pigt3  26447  pige3  26448  pige3ALT  26449  ang180lem2  26740  1cubrlem  26771  log2cnv  26874  log2tlbnd  26875  log2ub  26879  cxploglim2  26909  basellem5  27015  basellem9  27019  ppiublem1  27133  ppiub  27135  chtub  27143  bposlem2  27216  bposlem3  27217  bposlem4  27218  bposlem5  27219  bposlem6  27220  bposlem8  27222  bposlem9  27223  lgsdir2lem1  27256  2lgslem3  27335  chebbnd1lem2  27401  chebbnd1lem3  27402  chebbnd1  27403  chto1ub  27407  dchrvmasumlem2  27429  dchrvmasumlema  27431  dchrvmasumiflem1  27432  mulog2sumlem2  27466  pntibndlem1  27520  pntibndlem2  27522  pntlemb  27528  pntlemk  27537  pntlemo  27538  istrkg3ld  28432  tgcgr4  28502  axlowdimlem16  28928  axlowdimlem17  28929  axlowdim  28932  usgrexmplef  29230  upgr4cycl4dv4e  30155  konigsbergiedgw  30218  konigsberglem1  30222  konigsberglem2  30223  konigsberglem3  30224  konigsberglem4  30225  frgrogt3nreg  30367  friendshipgt3  30368  friendship  30369  ex-dif  30393  ex-in  30395  ex-fl  30417  ex-ceil  30418  ex-gcd  30427  threehalves  32885  iconstr  33769  2sqr3minply  33783  cos9thpiminplylem3  33787  cos9thpinconstrlem1  33792  prodfzo03  34606  hgt750lem  34654  hgt750lem2  34655  hgt750leme  34661  cusgracyclt3v  35168  problem3  35679  problem5  35681  poimirlem9  37648  itg2addnclem2  37691  heiborlem5  37834  heiborlem6  37835  heiborlem7  37836  heiborlem8  37837  3lexlogpow5ineq2  42067  3lexlogpow5ineq4  42068  3lexlogpow5ineq3  42069  3lexlogpow2ineq1  42070  3lexlogpow2ineq2  42071  3lexlogpow5ineq5  42072  aks4d1lem1  42074  aks4d1p1p3  42081  aks4d1p1p2  42082  aks4d1p1p4  42083  aks4d1p1p6  42085  aks4d1p1p5  42087  aks4d1p1  42088  aks4d1p2  42089  aks4d1p3  42090  aks4d1p5  42092  aks4d1p6  42093  aks4d1p7d1  42094  aks4d1p7  42095  aks4d1p8  42099  aks4d1p9  42100  2np3bcnp1  42156  2ap1caineq  42157  aks6d1c7lem1  42192  aks6d1c7lem2  42193  aks6d1c7  42196  aks5lem6  42204  aks5lem8  42213  acos1half  42370  sn-0ne2  42418  3cubeslem2  42697  3cubeslem4  42701  jm2.23  43008  jm2.20nn  43009  lt4addmuld  45326  stoweidlem11  46028  stoweidlem13  46030  stoweidlem26  46043  stoweidlem34  46051  stoweidlem42  46059  stoweidlem59  46076  stoweidlem62  46079  stoweid  46080  wallispilem4  46085  fourierdlem87  46210  smfmullem4  46811  modm2nep1  47376  modm1nep2  47378  fmtnoge3  47540  fmtnoprmfac2lem1  47576  31prm  47607  9fppr8  47747  fpprel2  47751  nfermltl8rev  47752  nfermltl2rev  47753  gbegt5  47771  gboge9  47774  sbgoldbwt  47787  sbgoldbst  47788  sbgoldbalt  47791  sbgoldbo  47797  nnsum3primes4  47798  nnsum4primes4  47799  nnsum4primesprm  47801  nnsum3primesgbe  47802  nnsum4primesgbe  47803  nnsum3primesle9  47804  nnsum4primesle9  47805  evengpop3  47808  evengpoap3  47809  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  wtgoldbnnsum4prm  47812  bgoldbnnsum3prm  47814  cycl3grtri  47957  usgrexmpl1lem  48031  usgrexmpl2lem  48036  usgrexmpl2nb3  48044  usgrexmpl2nb4  48045  usgrexmpl2nb5  48046  usgrexmpl2trifr  48047  gpgusgralem  48066  gpg3nbgrvtx0  48086  gpg3kgrtriexlem1  48093  gpg3kgrtriexlem3  48095  gpg3kgrtriexlem4  48096  gpg3kgrtriexlem6  48098  pgnbgreunbgrlem2lem1  48124  pgnbgreunbgrlem2lem2  48125  pgrpgt2nabl  48376  ackval42  48707  sepfsepc  48938