Theorem 3re 12348

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 12331	. 2 ⊢ 3 = (2 + 1)
2		2re 12342	. . 3 ⊢ 2 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126  1c1 11128   + caddc 11130  2c2 12322  3c3 12323

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331

This theorem is used by:  4re  12352  2le3  12442  1lt3  12443  3lt4  12444  2lt4  12445  3lt5  12448  3lt6  12453  2lt6  12454  3lt7  12459  2lt7  12460  3lt8  12466  2lt8  12467  3lt9  12474  2lt9  12475  1le3  12482  3halfnz  12703  3lt10  12882  5eluz3  12935  uzuzle23  12936  uzuzle34  12938  uz3m2nn  12946  nn01to3  12993  3rp  13051  fz0to4untppr  13688  fz0to5un2tp  13689  expnass  14275  hashtpg  14553  hash3tpde  14561  01sqrexlem7  15338  sqrt9  15363  caucvgrlem  15763  bpoly4  16148  ef01bndlem  16275  sin01bnd  16276  cos2bnd  16279  sin01gt0  16281  cos01gt0  16282  egt2lt3  16297  rpnnen2lem3  16307  rpnnen2lem4  16308  rpnnen2lem9  16313  flodddiv4  16508  ge2nprmge4  16795  starvndxnmulrndx  17394  scandxnmulrndx  17406  vscandxnmulrndx  17411  ipndxnmulrndx  17422  tsetndxnmulrndx  17446  plendxnmulrndx  17460  dsndxnmulrndx  17479  slotsdifunifndx  17489  vitalilem4  25842  dveflem  26209  sincosq3sgn  26741  sincosq4sgn  26742  tangtx  26746  sincos6thpi  26756  pigt3  26758  pige3  26759  pige3ALT  26760  ang180lem2  27050  1cubrlem  27081  log2cnv  27184  log2tlbnd  27185  log2ub  27189  cxploglim2  27218  basellem5  27324  basellem9  27328  ppiublem1  27441  ppiub  27443  chtub  27451  bposlem2  27524  bposlem3  27525  bposlem4  27526  bposlem5  27527  bposlem6  27528  bposlem8  27530  bposlem9  27531  lgsdir2lem1  27564  2lgslem3  27643  chebbnd1lem2  27709  chebbnd1lem3  27710  chebbnd1  27711  chto1ub  27715  dchrvmasumlem2  27737  dchrvmasumlema  27739  dchrvmasumiflem1  27740  mulog2sumlem2  27774  pntibndlem1  27828  pntibndlem2  27830  pntlemb  27836  pntlemk  27845  pntlemo  27846  istrkg3ld  28805  tgcgr4  28876  axlowdimlem16  29417  axlowdimlem17  29418  axlowdim  29421  usgrexmplef  29722  upgr4cycl4dv4e  30668  konigsbergiedgw  30731  konigsberglem1  30735  konigsberglem2  30736  konigsberglem3  30737  konigsberglem4  30738  frgrogt3nreg  30880  friendshipgt3  30881  friendship  30882  ex-dif  30906  ex-in  30908  ex-fl  30930  ex-ceil  30931  ex-gcd  30940  threehalves  33363  iconstr  34279  2sqr3minply  34293  cos9thpiminplylem3  34297  cos9thpinconstrlem1  34302  prodfzo03  35114  hgt750lem  35162  hgt750lem2  35163  hgt750leme  35169  cusgracyclt3v  35738  problem3  36249  problem5  36251  poimirlem9  38381  itg2addnclem2  38424  heiborlem5  38568  heiborlem6  38569  heiborlem7  38570  heiborlem8  38571  3lexlogpow5ineq2  42924  3lexlogpow5ineq4  42925  3lexlogpow5ineq3  42926  3lexlogpow2ineq1  42927  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  aks4d1lem1  42931  aks4d1p1p3  42938  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p5  42944  aks4d1p1  42945  aks4d1p2  42946  aks4d1p3  42947  aks4d1p5  42949  aks4d1p6  42950  aks4d1p7d1  42951  aks4d1p7  42952  aks4d1p8  42956  aks4d1p9  42957  2np3bcnp1  43013  2ap1caineq  43014  aks6d1c7lem1  43049  aks6d1c7lem2  43050  aks6d1c7  43053  aks5lem6  43061  aks5lem8  43070  acos1half  43236  sn-0ne2  43284  3cubeslem2  43533  3cubeslem4  43537  jm2.23  43840  lt4addmuld  46142  stoweidlem11  46842  stoweidlem13  46844  stoweidlem26  46857  stoweidlem34  46865  stoweidlem42  46873  stoweidlem59  46890  stoweidlem62  46893  stoweid  46894  wallispilem4  46899  fourierdlem87  47024  smfmullem4  47625  modm2nep1  48263  modm1nep2  48265  fmtnoge3  48436  fmtnoprmfac2lem1  48472  31prm  48503  9fppr8  48656  fpprel2  48660  nfermltl8rev  48661  nfermltl2rev  48662  gbegt5  48680  gboge9  48683  sbgoldbwt  48696  sbgoldbst  48697  sbgoldbalt  48700  sbgoldbo  48706  nnsum3primes4  48707  nnsum4primes4  48708  nnsum4primesprm  48710  nnsum3primesgbe  48711  nnsum4primesgbe  48712  nnsum3primesle9  48713  nnsum4primesle9  48714  evengpop3  48717  evengpoap3  48718  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  cycl3grtri  48866  usgrexmpl1lem  48940  usgrexmpl2lem  48945  usgrexmpl2nb3  48953  usgrexmpl2nb4  48954  usgrexmpl2nb5  48955  usgrexmpl2trifr  48956  gpgusgralem  48975  gpg3nbgrvtx0  48995  gpg3kgrtriexlem1  49002  gpg3kgrtriexlem3  49004  gpg3kgrtriexlem4  49005  gpg3kgrtriexlem6  49007  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgrpgt2nabl  49299  ackval42  49629  sepfsepc  49857  veronesev3lem  50811  veronesev4lem  50812  veronesev5lem  50813  veronesev6lem  50814  veronesevrowd  50815  veroquadgsumlem  50819