Theorem 3re 12317

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 12300	. 2 ⊢ 3 = (2 + 1)
2		2re 12311	. . 3 ⊢ 2 ∈ ℝ
3		1re 11204	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11220	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2865	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7408  ℝcr 11095  1c1 11097   + caddc 11099  2c2 12291  3c3 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rrecex 11168  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-ov 7411  df-2 12299  df-3 12300

This theorem is referenced by:  4re  12321  2le3  12411  1lt3  12412  3lt4  12413  2lt4  12414  3lt5  12417  3lt6  12422  2lt6  12423  3lt7  12428  2lt7  12429  3lt8  12435  2lt8  12436  3lt9  12443  2lt9  12444  1le3  12451  3halfnz  12671  3lt10  12850  5eluz3  12903  uzuzle23  12904  uzuzle34  12906  uz3m2nn  12914  nn01to3  12961  3rp  13018  fz0to4untppr  13654  fz0to5un2tp  13655  expnass  14240  hashtpg  14518  hash3tpde  14526  01sqrexlem7  15295  sqrt9  15320  caucvgrlem  15720  bpoly4  16109  ef01bndlem  16236  sin01bnd  16237  cos2bnd  16240  sin01gt0  16242  cos01gt0  16243  egt2lt3  16258  rpnnen2lem3  16268  rpnnen2lem4  16269  rpnnen2lem9  16274  flodddiv4  16469  ge2nprmge4  16756  starvndxnmulrndx  17355  scandxnmulrndx  17367  vscandxnmulrndx  17372  ipndxnmulrndx  17383  tsetndxnmulrndx  17407  plendxnmulrndx  17421  dsndxnmulrndx  17440  slotsdifunifndx  17450  vitalilem4  25735  dveflem  26103  sincosq3sgn  26627  sincosq4sgn  26628  tangtx  26632  sincos6thpi  26643  pigt3  26645  pige3  26646  pige3ALT  26647  ang180lem2  26937  1cubrlem  26968  log2cnv  27071  log2tlbnd  27072  log2ub  27076  cxploglim2  27105  basellem5  27211  basellem9  27215  ppiublem1  27328  ppiub  27330  chtub  27338  bposlem2  27411  bposlem3  27412  bposlem4  27413  bposlem5  27414  bposlem6  27415  bposlem8  27417  bposlem9  27418  lgsdir2lem1  27451  2lgslem3  27530  chebbnd1lem2  27596  chebbnd1lem3  27597  chebbnd1  27598  chto1ub  27602  dchrvmasumlem2  27624  dchrvmasumlema  27626  dchrvmasumiflem1  27627  mulog2sumlem2  27661  pntibndlem1  27715  pntibndlem2  27717  pntlemb  27723  pntlemk  27732  pntlemo  27733  istrkg3ld  28692  tgcgr4  28762  axlowdimlem16  29244  axlowdimlem17  29245  axlowdim  29248  usgrexmplef  29546  upgr4cycl4dv4e  30473  konigsbergiedgw  30536  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  konigsberglem4  30543  frgrogt3nreg  30685  friendshipgt3  30686  friendship  30687  ex-dif  30711  ex-in  30713  ex-fl  30735  ex-ceil  30736  ex-gcd  30745  threehalves  33171  iconstr  34097  2sqr3minply  34111  cos9thpiminplylem3  34115  cos9thpinconstrlem1  34120  prodfzo03  34931  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  cusgracyclt3v  35543  problem3  36054  problem5  36056  poimirlem9  38163  itg2addnclem2  38206  heiborlem5  38349  heiborlem6  38350  heiborlem7  38351  heiborlem8  38352  3lexlogpow5ineq2  42707  3lexlogpow5ineq4  42708  3lexlogpow5ineq3  42709  3lexlogpow2ineq1  42710  3lexlogpow2ineq2  42711  3lexlogpow5ineq5  42712  aks4d1lem1  42714  aks4d1p1p3  42721  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p2  42729  aks4d1p3  42730  aks4d1p5  42732  aks4d1p6  42733  aks4d1p7d1  42734  aks4d1p7  42735  aks4d1p8  42739  aks4d1p9  42740  2np3bcnp1  42796  2ap1caineq  42797  aks6d1c7lem1  42832  aks6d1c7lem2  42833  aks6d1c7  42836  aks5lem6  42844  aks5lem8  42853  acos1half  43002  sn-0ne2  43050  3cubeslem2  43301  3cubeslem4  43305  jm2.23  43608  lt4addmuld  45910  stoweidlem11  46610  stoweidlem13  46612  stoweidlem26  46625  stoweidlem34  46633  stoweidlem42  46641  stoweidlem59  46658  stoweidlem62  46661  stoweid  46662  wallispilem4  46667  fourierdlem87  46792  smfmullem4  47393  modm2nep1  47991  modm1nep2  47993  fmtnoge3  48164  fmtnoprmfac2lem1  48200  31prm  48231  9fppr8  48384  fpprel2  48388  nfermltl8rev  48389  nfermltl2rev  48390  gbegt5  48408  gboge9  48411  sbgoldbwt  48424  sbgoldbst  48425  sbgoldbalt  48428  sbgoldbo  48434  nnsum3primes4  48435  nnsum4primes4  48436  nnsum4primesprm  48438  nnsum3primesgbe  48439  nnsum4primesgbe  48440  nnsum3primesle9  48441  nnsum4primesle9  48442  evengpop3  48445  evengpoap3  48446  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  wtgoldbnnsum4prm  48449  bgoldbnnsum3prm  48451  cycl3grtri  48594  usgrexmpl1lem  48668  usgrexmpl2lem  48673  usgrexmpl2nb3  48681  usgrexmpl2nb4  48682  usgrexmpl2nb5  48683  usgrexmpl2trifr  48684  gpgusgralem  48703  gpg3nbgrvtx0  48723  gpg3kgrtriexlem1  48730  gpg3kgrtriexlem3  48732  gpg3kgrtriexlem4  48733  gpg3kgrtriexlem6  48735  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgrpgt2nabl  49024  ackval42  49354  sepfsepc  49584