Theorem 3re 12316

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 12299	. 2 ⊢ 3 = (2 + 1)
2		2re 12310	. . 3 ⊢ 2 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  2c2 12290  3c3 12291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299

This theorem is referenced by:  4re  12320  2le3  12410  1lt3  12411  3lt4  12412  2lt4  12413  3lt5  12416  3lt6  12421  2lt6  12422  3lt7  12427  2lt7  12428  3lt8  12434  2lt8  12435  3lt9  12442  2lt9  12443  1le3  12450  3halfnz  12670  3lt10  12849  5eluz3  12902  uzuzle23  12903  uzuzle34  12905  uz3m2nn  12913  nn01to3  12960  3rp  13017  fz0to4untppr  13654  fz0to5un2tp  13655  expnass  14240  hashtpg  14518  hash3tpde  14526  01sqrexlem7  15295  sqrt9  15320  caucvgrlem  15720  bpoly4  16108  ef01bndlem  16235  sin01bnd  16236  cos2bnd  16239  sin01gt0  16241  cos01gt0  16242  egt2lt3  16257  rpnnen2lem3  16267  rpnnen2lem4  16268  rpnnen2lem9  16273  flodddiv4  16468  ge2nprmge4  16755  starvndxnmulrndx  17354  scandxnmulrndx  17366  vscandxnmulrndx  17371  ipndxnmulrndx  17382  tsetndxnmulrndx  17406  plendxnmulrndx  17420  dsndxnmulrndx  17439  slotsdifunifndx  17449  vitalilem4  25770  dveflem  26138  sincosq3sgn  26665  sincosq4sgn  26666  tangtx  26670  sincos6thpi  26681  pigt3  26683  pige3  26684  pige3ALT  26685  ang180lem2  26975  1cubrlem  27006  log2cnv  27109  log2tlbnd  27110  log2ub  27114  cxploglim2  27143  basellem5  27249  basellem9  27253  ppiublem1  27366  ppiub  27368  chtub  27376  bposlem2  27449  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem8  27455  bposlem9  27456  lgsdir2lem1  27489  2lgslem3  27568  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  chto1ub  27640  dchrvmasumlem2  27662  dchrvmasumlema  27664  dchrvmasumiflem1  27665  mulog2sumlem2  27699  pntibndlem1  27753  pntibndlem2  27755  pntlemb  27761  pntlemk  27770  pntlemo  27771  istrkg3ld  28730  tgcgr4  28800  axlowdimlem16  29307  axlowdimlem17  29308  axlowdim  29311  usgrexmplef  29609  upgr4cycl4dv4e  30536  konigsbergiedgw  30599  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  konigsberglem4  30606  frgrogt3nreg  30748  friendshipgt3  30749  friendship  30750  ex-dif  30774  ex-in  30776  ex-fl  30798  ex-ceil  30799  ex-gcd  30808  threehalves  33234  iconstr  34156  2sqr3minply  34170  cos9thpiminplylem3  34174  cos9thpinconstrlem1  34179  prodfzo03  34990  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  cusgracyclt3v  35648  problem3  36159  problem5  36161  poimirlem9  38300  itg2addnclem2  38343  heiborlem5  38486  heiborlem6  38487  heiborlem7  38488  heiborlem8  38489  3lexlogpow5ineq2  42842  3lexlogpow5ineq4  42843  3lexlogpow5ineq3  42844  3lexlogpow2ineq1  42845  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1lem1  42849  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p5  42862  aks4d1p1  42863  aks4d1p2  42864  aks4d1p3  42865  aks4d1p5  42867  aks4d1p6  42868  aks4d1p7d1  42869  aks4d1p7  42870  aks4d1p8  42874  aks4d1p9  42875  2np3bcnp1  42931  2ap1caineq  42932  aks6d1c7lem1  42967  aks6d1c7lem2  42968  aks6d1c7  42971  aks5lem6  42979  aks5lem8  42988  acos1half  43139  sn-0ne2  43187  3cubeslem2  43436  3cubeslem4  43440  jm2.23  43743  lt4addmuld  46045  stoweidlem11  46745  stoweidlem13  46747  stoweidlem26  46760  stoweidlem34  46768  stoweidlem42  46776  stoweidlem59  46793  stoweidlem62  46796  stoweid  46797  wallispilem4  46802  fourierdlem87  46927  smfmullem4  47528  modm2nep1  48129  modm1nep2  48131  fmtnoge3  48302  fmtnoprmfac2lem1  48338  31prm  48369  9fppr8  48522  fpprel2  48526  nfermltl8rev  48527  nfermltl2rev  48528  gbegt5  48546  gboge9  48549  sbgoldbwt  48562  sbgoldbst  48563  sbgoldbalt  48566  sbgoldbo  48572  nnsum3primes4  48573  nnsum4primes4  48574  nnsum4primesprm  48576  nnsum3primesgbe  48577  nnsum4primesgbe  48578  nnsum3primesle9  48579  nnsum4primesle9  48580  evengpop3  48583  evengpoap3  48584  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  wtgoldbnnsum4prm  48587  bgoldbnnsum3prm  48589  cycl3grtri  48732  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb3  48819  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  usgrexmpl2trifr  48822  gpgusgralem  48841  gpg3nbgrvtx0  48861  gpg3kgrtriexlem1  48868  gpg3kgrtriexlem3  48870  gpg3kgrtriexlem4  48871  gpg3kgrtriexlem6  48873  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgrpgt2nabl  49166  ackval42  49496  sepfsepc  49726