Theorem 3re 12343

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 12327	. 2 ⊢ 3 = (2 + 1)
2		2re 12337	. . 3 ⊢ 2 ∈ ℝ
3		1re 11258	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11273	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2834	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155  2c2 12318  3c3 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327

This theorem is referenced by:  4re  12347  3ne0  12369  4pos  12370  1lt3  12436  3lt4  12437  2lt4  12438  3lt5  12441  3lt6  12446  2lt6  12447  3lt7  12452  2lt7  12453  3lt8  12459  2lt8  12460  3lt9  12467  2lt9  12468  1le3  12475  3halfnz  12694  3lt10  12867  2lt10  12868  eluz4eluz3  12923  5eluz3  12924  uzuzle23  12928  uz3m2nn  12930  nn01to3  12980  3rp  13037  fz0to4untppr  13666  fz0to5un2tp  13667  expnass  14243  hashtpg  14520  hash3tpde  14528  01sqrexlem7  15283  sqrt9  15308  caucvgrlem  15705  bpoly4  16091  ef01bndlem  16216  sin01bnd  16217  cos2bnd  16220  sin01gt0  16222  cos01gt0  16223  egt2lt3  16238  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  flodddiv4  16448  ge2nprmge4  16734  starvndxnmulrndx  17351  scandxnmulrndx  17363  vscandxnmulrndx  17368  ipndxnmulrndx  17379  tsetndxnmulrndx  17403  plendxnmulrndx  17417  dsndxnmulrndx  17436  slotsdifunifndx  17446  cnfldfunALTOLDOLD  21410  matscaOLD  22435  matvscaOLD  22437  vitalilem4  25659  dveflem  26031  sincosq3sgn  26556  sincosq4sgn  26557  tangtx  26561  sincos6thpi  26572  pigt3  26574  pige3  26575  pige3ALT  26576  ang180lem2  26867  1cubrlem  26898  log2cnv  27001  log2tlbnd  27002  log2ub  27006  cxploglim2  27036  basellem5  27142  basellem9  27146  ppiublem1  27260  ppiub  27262  chtub  27270  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem1  27383  2lgslem3  27462  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chto1ub  27534  dchrvmasumlem2  27556  dchrvmasumlema  27558  dchrvmasumiflem1  27559  mulog2sumlem2  27593  pntibndlem1  27647  pntibndlem2  27649  pntlemb  27655  pntlemk  27664  pntlemo  27665  istrkg3ld  28483  tgcgr4  28553  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  usgrexmplef  29290  upgr4cycl4dv4e  30213  konigsbergiedgw  30276  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  konigsberglem4  30283  frgrogt3nreg  30425  friendshipgt3  30426  friendship  30427  ex-dif  30451  ex-in  30453  ex-fl  30475  ex-ceil  30476  ex-gcd  30485  threehalves  32881  resvmulrOLD  33345  2sqr3minply  33752  prodfzo03  34596  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  cusgracyclt3v  35140  problem3  35651  problem5  35653  poimirlem9  37615  itg2addnclem2  37658  heiborlem5  37801  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  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  2xp3dxp2ge1d  42222  acos1half  42366  sn-0ne2  42412  3cubeslem2  42672  3cubeslem4  42676  jm2.23  42984  jm2.20nn  42985  mnringscadOLD  44218  mnringvscadOLD  44220  lt4addmuld  45256  stoweidlem11  45966  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  stoweidlem42  45997  stoweidlem59  46014  stoweidlem62  46017  stoweid  46018  wallispilem4  46023  fourierdlem87  46148  smfmullem4  46749  fmtnoge3  47454  fmtnoprmfac2lem1  47490  31prm  47521  9fppr8  47661  fpprel2  47665  nfermltl8rev  47666  nfermltl2rev  47667  gbegt5  47685  gboge9  47688  sbgoldbwt  47701  sbgoldbst  47702  sbgoldbalt  47705  sbgoldbo  47711  nnsum3primes4  47712  nnsum4primes4  47713  nnsum4primesprm  47715  nnsum3primesgbe  47716  nnsum4primesgbe  47717  nnsum3primesle9  47718  nnsum4primesle9  47719  evengpop3  47722  evengpoap3  47723  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  gpgusgralem  47945  gpg3nbgrvtx0  47966  pgrpgt2nabl  48210  ackval42  48545  sepfsepc  48723