Theorem 3re 12242

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 12226	. 2 ⊢ 3 = (2 + 1)
2		2re 12236	. . 3 ⊢ 2 ∈ ℝ
3		1re 11150	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11165	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  2c2 12217  3c3 12218

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226

This theorem is referenced by:  4re  12246  4pos  12269  1lt3  12330  3lt4  12331  2lt4  12332  3lt5  12335  3lt6  12340  2lt6  12341  3lt7  12346  2lt7  12347  3lt8  12353  2lt8  12354  3lt9  12361  2lt9  12362  1le3  12369  3halfnz  12589  3lt10  12762  2lt10  12763  5eluz3  12818  uzuzle23  12819  uzuzle34  12821  uz3m2nn  12829  nn01to3  12876  3rp  12933  fz0to4untppr  13567  fz0to5un2tp  13568  expnass  14149  hashtpg  14426  hash3tpde  14434  01sqrexlem7  15190  sqrt9  15215  caucvgrlem  15615  bpoly4  16001  ef01bndlem  16128  sin01bnd  16129  cos2bnd  16132  sin01gt0  16134  cos01gt0  16135  egt2lt3  16150  rpnnen2lem3  16160  rpnnen2lem4  16161  rpnnen2lem9  16166  flodddiv4  16361  ge2nprmge4  16647  starvndxnmulrndx  17245  scandxnmulrndx  17257  vscandxnmulrndx  17262  ipndxnmulrndx  17273  tsetndxnmulrndx  17297  plendxnmulrndx  17311  dsndxnmulrndx  17330  slotsdifunifndx  17340  vitalilem4  25545  dveflem  25916  sincosq3sgn  26442  sincosq4sgn  26443  tangtx  26447  sincos6thpi  26458  pigt3  26460  pige3  26461  pige3ALT  26462  ang180lem2  26753  1cubrlem  26784  log2cnv  26887  log2tlbnd  26888  log2ub  26892  cxploglim2  26922  basellem5  27028  basellem9  27032  ppiublem1  27146  ppiub  27148  chtub  27156  bposlem2  27229  bposlem3  27230  bposlem4  27231  bposlem5  27232  bposlem6  27233  bposlem8  27235  bposlem9  27236  lgsdir2lem1  27269  2lgslem3  27348  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  chto1ub  27420  dchrvmasumlem2  27442  dchrvmasumlema  27444  dchrvmasumiflem1  27445  mulog2sumlem2  27479  pntibndlem1  27533  pntibndlem2  27535  pntlemb  27541  pntlemk  27550  pntlemo  27551  istrkg3ld  28441  tgcgr4  28511  axlowdimlem16  28937  axlowdimlem17  28938  axlowdim  28941  usgrexmplef  29239  upgr4cycl4dv4e  30164  konigsbergiedgw  30227  konigsberglem1  30231  konigsberglem2  30232  konigsberglem3  30233  konigsberglem4  30234  frgrogt3nreg  30376  friendshipgt3  30377  friendship  30378  ex-dif  30402  ex-in  30404  ex-fl  30426  ex-ceil  30427  ex-gcd  30436  threehalves  32885  iconstr  33749  2sqr3minply  33763  cos9thpiminplylem3  33767  cos9thpinconstrlem1  33772  prodfzo03  34587  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  cusgracyclt3v  35136  problem3  35647  problem5  35649  poimirlem9  37616  itg2addnclem2  37659  heiborlem5  37802  heiborlem6  37803  heiborlem7  37804  heiborlem8  37805  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  2np3bcnp1  42125  2ap1caineq  42126  aks6d1c7lem1  42161  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem6  42173  aks5lem8  42182  acos1half  42339  sn-0ne2  42387  3cubeslem2  42666  3cubeslem4  42670  jm2.23  42978  jm2.20nn  42979  lt4addmuld  45297  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  47939  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgusgralem  48040  gpg3nbgrvtx0  48060  gpg3kgrtriexlem1  48067  gpg3kgrtriexlem3  48069  gpg3kgrtriexlem4  48070  gpg3kgrtriexlem6  48072  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgrpgt2nabl  48347  ackval42  48678  sepfsepc  48909