Theorem 3re 12266

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 12250	. 2 ⊢ 3 = (2 + 1)
2		2re 12260	. . 3 ⊢ 2 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  2c2 12241  3c3 12242

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 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250

This theorem is referenced by:  4re  12270  4pos  12293  1lt3  12354  3lt4  12355  2lt4  12356  3lt5  12359  3lt6  12364  2lt6  12365  3lt7  12370  2lt7  12371  3lt8  12377  2lt8  12378  3lt9  12385  2lt9  12386  1le3  12393  3halfnz  12613  3lt10  12786  2lt10  12787  5eluz3  12842  uzuzle23  12843  uzuzle34  12845  uz3m2nn  12853  nn01to3  12900  3rp  12957  fz0to4untppr  13591  fz0to5un2tp  13592  expnass  14173  hashtpg  14450  hash3tpde  14458  01sqrexlem7  15214  sqrt9  15239  caucvgrlem  15639  bpoly4  16025  ef01bndlem  16152  sin01bnd  16153  cos2bnd  16156  sin01gt0  16158  cos01gt0  16159  egt2lt3  16174  rpnnen2lem3  16184  rpnnen2lem4  16185  rpnnen2lem9  16190  flodddiv4  16385  ge2nprmge4  16671  starvndxnmulrndx  17269  scandxnmulrndx  17281  vscandxnmulrndx  17286  ipndxnmulrndx  17297  tsetndxnmulrndx  17321  plendxnmulrndx  17335  dsndxnmulrndx  17354  slotsdifunifndx  17364  vitalilem4  25512  dveflem  25883  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sincos6thpi  26425  pigt3  26427  pige3  26428  pige3ALT  26429  ang180lem2  26720  1cubrlem  26751  log2cnv  26854  log2tlbnd  26855  log2ub  26859  cxploglim2  26889  basellem5  26995  basellem9  26999  ppiublem1  27113  ppiub  27115  chtub  27123  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  2lgslem3  27315  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chto1ub  27387  dchrvmasumlem2  27409  dchrvmasumlema  27411  dchrvmasumiflem1  27412  mulog2sumlem2  27446  pntibndlem1  27500  pntibndlem2  27502  pntlemb  27508  pntlemk  27517  pntlemo  27518  istrkg3ld  28388  tgcgr4  28458  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  usgrexmplef  29186  upgr4cycl4dv4e  30114  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem4  30184  frgrogt3nreg  30326  friendshipgt3  30327  friendship  30328  ex-dif  30352  ex-in  30354  ex-fl  30376  ex-ceil  30377  ex-gcd  30386  threehalves  32835  iconstr  33756  2sqr3minply  33770  cos9thpiminplylem3  33774  cos9thpinconstrlem1  33779  prodfzo03  34594  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  cusgracyclt3v  35143  problem3  35654  problem5  35656  poimirlem9  37623  itg2addnclem2  37666  heiborlem5  37809  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  aks5lem8  42189  acos1half  42346  sn-0ne2  42394  3cubeslem2  42673  3cubeslem4  42677  jm2.23  42985  jm2.20nn  42986  lt4addmuld  45304  stoweidlem11  46009  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweidlem42  46040  stoweidlem59  46057  stoweidlem62  46060  stoweid  46061  wallispilem4  46066  fourierdlem87  46191  smfmullem4  46792  modm2nep1  47367  modm1nep2  47369  fmtnoge3  47531  fmtnoprmfac2lem1  47567  31prm  47598  9fppr8  47738  fpprel2  47742  nfermltl8rev  47743  nfermltl2rev  47744  gbegt5  47762  gboge9  47765  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbalt  47782  sbgoldbo  47788  nnsum3primes4  47789  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum3primesgbe  47793  nnsum4primesgbe  47794  nnsum3primesle9  47795  nnsum4primesle9  47796  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  cycl3grtri  47946  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgusgralem  48047  gpg3nbgrvtx0  48067  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgrpgt2nabl  48354  ackval42  48685  sepfsepc  48916