Theorem 3re 12208

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 12192	. 2 ⊢ 3 = (2 + 1)
2		2re 12202	. . 3 ⊢ 2 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  2c2 12183  3c3 12184

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 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192

This theorem is referenced by:  4re  12212  4pos  12235  1lt3  12296  3lt4  12297  2lt4  12298  3lt5  12301  3lt6  12306  2lt6  12307  3lt7  12312  2lt7  12313  3lt8  12319  2lt8  12320  3lt9  12327  2lt9  12328  1le3  12335  3halfnz  12555  3lt10  12728  2lt10  12729  5eluz3  12784  uzuzle23  12785  uzuzle34  12787  uz3m2nn  12795  nn01to3  12842  3rp  12899  fz0to4untppr  13533  fz0to5un2tp  13534  expnass  14115  hashtpg  14392  hash3tpde  14400  01sqrexlem7  15155  sqrt9  15180  caucvgrlem  15580  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos2bnd  16097  sin01gt0  16099  cos01gt0  16100  egt2lt3  16115  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  flodddiv4  16326  ge2nprmge4  16612  starvndxnmulrndx  17210  scandxnmulrndx  17222  vscandxnmulrndx  17227  ipndxnmulrndx  17238  tsetndxnmulrndx  17262  plendxnmulrndx  17276  dsndxnmulrndx  17295  slotsdifunifndx  17305  vitalilem4  25510  dveflem  25881  sincosq3sgn  26407  sincosq4sgn  26408  tangtx  26412  sincos6thpi  26423  pigt3  26425  pige3  26426  pige3ALT  26427  ang180lem2  26718  1cubrlem  26749  log2cnv  26852  log2tlbnd  26853  log2ub  26857  cxploglim2  26887  basellem5  26993  basellem9  26997  ppiublem1  27111  ppiub  27113  chtub  27121  bposlem2  27194  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem8  27200  bposlem9  27201  lgsdir2lem1  27234  2lgslem3  27313  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  chto1ub  27385  dchrvmasumlem2  27407  dchrvmasumlema  27409  dchrvmasumiflem1  27410  mulog2sumlem2  27444  pntibndlem1  27498  pntibndlem2  27500  pntlemb  27506  pntlemk  27515  pntlemo  27516  istrkg3ld  28406  tgcgr4  28476  axlowdimlem16  28902  axlowdimlem17  28903  axlowdim  28906  usgrexmplef  29204  upgr4cycl4dv4e  30129  konigsbergiedgw  30192  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  konigsberglem4  30199  frgrogt3nreg  30341  friendshipgt3  30342  friendship  30343  ex-dif  30367  ex-in  30369  ex-fl  30391  ex-ceil  30392  ex-gcd  30401  threehalves  32856  iconstr  33739  2sqr3minply  33753  cos9thpiminplylem3  33757  cos9thpinconstrlem1  33762  prodfzo03  34577  hgt750lem  34625  hgt750lem2  34626  hgt750leme  34632  cusgracyclt3v  35139  problem3  35650  problem5  35652  poimirlem9  37619  itg2addnclem2  37662  heiborlem5  37805  heiborlem6  37806  heiborlem7  37807  heiborlem8  37808  3lexlogpow5ineq2  42038  3lexlogpow5ineq4  42039  3lexlogpow5ineq3  42040  3lexlogpow2ineq1  42041  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  aks4d1lem1  42045  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p5  42058  aks4d1p1  42059  aks4d1p2  42060  aks4d1p3  42061  aks4d1p5  42063  aks4d1p6  42064  aks4d1p7d1  42065  aks4d1p7  42066  aks4d1p8  42070  aks4d1p9  42071  2np3bcnp1  42127  2ap1caineq  42128  aks6d1c7lem1  42163  aks6d1c7lem2  42164  aks6d1c7  42167  aks5lem6  42175  aks5lem8  42184  acos1half  42341  sn-0ne2  42389  3cubeslem2  42668  3cubeslem4  42672  jm2.23  42979  jm2.20nn  42980  lt4addmuld  45298  stoweidlem11  46002  stoweidlem13  46004  stoweidlem26  46017  stoweidlem34  46025  stoweidlem42  46033  stoweidlem59  46050  stoweidlem62  46053  stoweid  46054  wallispilem4  46059  fourierdlem87  46184  smfmullem4  46785  modm2nep1  47360  modm1nep2  47362  fmtnoge3  47524  fmtnoprmfac2lem1  47560  31prm  47591  9fppr8  47731  fpprel2  47735  nfermltl8rev  47736  nfermltl2rev  47737  gbegt5  47755  gboge9  47758  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbalt  47775  sbgoldbo  47781  nnsum3primes4  47782  nnsum4primes4  47783  nnsum4primesprm  47785  nnsum3primesgbe  47786  nnsum4primesgbe  47787  nnsum3primesle9  47788  nnsum4primesle9  47789  evengpop3  47792  evengpoap3  47793  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  cycl3grtri  47941  usgrexmpl1lem  48015  usgrexmpl2lem  48020  usgrexmpl2nb3  48028  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030  usgrexmpl2trifr  48031  gpgusgralem  48050  gpg3nbgrvtx0  48070  gpg3kgrtriexlem1  48077  gpg3kgrtriexlem3  48079  gpg3kgrtriexlem4  48080  gpg3kgrtriexlem6  48082  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgrpgt2nabl  48360  ackval42  48691  sepfsepc  48922