Theorem 3re 12273

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 12257	. 2 ⊢ 3 = (2 + 1)
2		2re 12267	. . 3 ⊢ 2 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11196	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078  2c2 12248  3c3 12249

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257

This theorem is referenced by:  4re  12277  4pos  12300  1lt3  12361  3lt4  12362  2lt4  12363  3lt5  12366  3lt6  12371  2lt6  12372  3lt7  12377  2lt7  12378  3lt8  12384  2lt8  12385  3lt9  12392  2lt9  12393  1le3  12400  3halfnz  12620  3lt10  12793  2lt10  12794  5eluz3  12849  uzuzle23  12850  uzuzle34  12852  uz3m2nn  12860  nn01to3  12907  3rp  12964  fz0to4untppr  13598  fz0to5un2tp  13599  expnass  14180  hashtpg  14457  hash3tpde  14465  01sqrexlem7  15221  sqrt9  15246  caucvgrlem  15646  bpoly4  16032  ef01bndlem  16159  sin01bnd  16160  cos2bnd  16163  sin01gt0  16165  cos01gt0  16166  egt2lt3  16181  rpnnen2lem3  16191  rpnnen2lem4  16192  rpnnen2lem9  16197  flodddiv4  16392  ge2nprmge4  16678  starvndxnmulrndx  17276  scandxnmulrndx  17288  vscandxnmulrndx  17293  ipndxnmulrndx  17304  tsetndxnmulrndx  17328  plendxnmulrndx  17342  dsndxnmulrndx  17361  slotsdifunifndx  17371  vitalilem4  25519  dveflem  25890  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sincos6thpi  26432  pigt3  26434  pige3  26435  pige3ALT  26436  ang180lem2  26727  1cubrlem  26758  log2cnv  26861  log2tlbnd  26862  log2ub  26866  cxploglim2  26896  basellem5  27002  basellem9  27006  ppiublem1  27120  ppiub  27122  chtub  27130  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  2lgslem3  27322  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  chto1ub  27394  dchrvmasumlem2  27416  dchrvmasumlema  27418  dchrvmasumiflem1  27419  mulog2sumlem2  27453  pntibndlem1  27507  pntibndlem2  27509  pntlemb  27515  pntlemk  27524  pntlemo  27525  istrkg3ld  28395  tgcgr4  28465  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  usgrexmplef  29193  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberglem4  30191  frgrogt3nreg  30333  friendshipgt3  30334  friendship  30335  ex-dif  30359  ex-in  30361  ex-fl  30383  ex-ceil  30384  ex-gcd  30393  threehalves  32842  iconstr  33763  2sqr3minply  33777  cos9thpiminplylem3  33781  cos9thpinconstrlem1  33786  prodfzo03  34601  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  cusgracyclt3v  35150  problem3  35661  problem5  35663  poimirlem9  37630  itg2addnclem2  37673  heiborlem5  37816  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1lem1  42057  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c7lem1  42175  aks6d1c7lem2  42176  aks6d1c7  42179  aks5lem6  42187  aks5lem8  42196  acos1half  42353  sn-0ne2  42401  3cubeslem2  42680  3cubeslem4  42684  jm2.23  42992  jm2.20nn  42993  lt4addmuld  45311  stoweidlem11  46016  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  stoweidlem42  46047  stoweidlem59  46064  stoweidlem62  46067  stoweid  46068  wallispilem4  46073  fourierdlem87  46198  smfmullem4  46799  modm2nep1  47371  modm1nep2  47373  fmtnoge3  47535  fmtnoprmfac2lem1  47571  31prm  47602  9fppr8  47742  fpprel2  47746  nfermltl8rev  47747  nfermltl2rev  47748  gbegt5  47766  gboge9  47769  sbgoldbwt  47782  sbgoldbst  47783  sbgoldbalt  47786  sbgoldbo  47792  nnsum3primes4  47793  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum3primesgbe  47797  nnsum4primesgbe  47798  nnsum3primesle9  47799  nnsum4primesle9  47800  evengpop3  47803  evengpoap3  47804  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpgusgralem  48051  gpg3nbgrvtx0  48071  gpg3kgrtriexlem1  48078  gpg3kgrtriexlem3  48080  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgrpgt2nabl  48358  ackval42  48689  sepfsepc  48920