Theorem 3re 12433

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 12416	. 2 ⊢ 3 = (2 + 1)
2		2re 12427	. . 3 ⊢ 2 ∈ ℝ
3		1re 11318	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11334	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213  2c2 12407  3c3 12408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416

This theorem is used by:  4re  12437  2le3  12527  1lt3  12528  3lt4  12529  2lt4  12530  3lt5  12533  3lt6  12538  2lt6  12539  3lt7  12544  2lt7  12545  3lt8  12551  2lt8  12552  3lt9  12559  2lt9  12560  1le3  12567  3halfnz  12788  3lt10  12967  5eluz3  13020  uzuzle23  13021  uzuzle34  13023  uz3m2nn  13031  nn01to3  13078  3rp  13136  fz0to4untppr  13774  fz0to5un2tp  13775  expnass  14362  hashtpg  14640  hash3tpde  14648  01sqrexlem7  15427  sqrt9  15452  caucvgrlem  15852  bpoly4  16237  ef01bndlem  16364  sin01bnd  16365  cos2bnd  16368  sin01gt0  16370  cos01gt0  16371  egt2lt3  16386  rpnnen2lem3  16396  rpnnen2lem4  16397  rpnnen2lem9  16402  flodddiv4  16597  ge2nprmge4  16889  starvndxnmulrndx  17489  scandxnmulrndx  17501  vscandxnmulrndx  17506  ipndxnmulrndx  17517  tsetndxnmulrndx  17541  plendxnmulrndx  17555  dsndxnmulrndx  17574  slotsdifunifndx  17584  vitalilem4  25944  dveflem  26311  sincosq3sgn  26841  sincosq4sgn  26842  tangtx  26846  sincos6thpi  26856  pigt3  26858  pige3  26859  pige3ALT  26860  ang180lem2  27150  1cubrlem  27181  log2cnv  27284  log2tlbnd  27285  log2ub  27289  cxploglim2  27318  basellem5  27424  basellem9  27428  ppiublem1  27541  ppiub  27543  chtub  27551  bposlem2  27624  bposlem3  27625  bposlem4  27626  bposlem5  27627  bposlem6  27628  bposlem8  27630  bposlem9  27631  lgsdir2lem1  27664  2lgslem3  27743  chebbnd1lem2  27809  chebbnd1lem3  27810  chebbnd1  27811  chto1ub  27815  dchrvmasumlem2  27837  dchrvmasumlema  27839  dchrvmasumiflem1  27840  mulog2sumlem2  27874  pntibndlem1  27928  pntibndlem2  27930  pntlemb  27936  pntlemk  27945  pntlemo  27946  fltoprmgt3  28008  tgcgr4  29006  axlowdimlem16  29547  axlowdimlem17  29548  axlowdim  29551  usgrexmplef  29852  upgr4cycl4dv4e  30798  konigsbergiedgw  30861  konigsberglem3  30867  konigsberglem4  30868  frgrogt3nreg  31010  friendshipgt3  31011  friendship  31012  ex-dif  31036  ex-in  31038  ex-fl  31060  ex-ceil  31061  ex-gcd  31070  threehalves  33534  iconstr  34451  2sqr3minply  34465  cos9thpiminplylem3  34469  cos9thpinconstrlem1  34474  prodfzo03  35285  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  cusgracyclt3v  36032  problem3  36553  problem5  36555  poimirlem9  38687  itg2addnclem2  38730  heiborlem5  38889  heiborlem6  38890  heiborlem7  38891  heiborlem8  38892  3lexlogpow5ineq2  43245  3lexlogpow5ineq4  43246  3lexlogpow5ineq3  43247  3lexlogpow2ineq1  43248  3lexlogpow2ineq2  43249  3lexlogpow5ineq5  43250  aks4d1lem1  43252  aks4d1p1p3  43259  aks4d1p1p2  43260  aks4d1p1p4  43261  aks4d1p1p6  43263  aks4d1p1p5  43265  aks4d1p1  43266  aks4d1p2  43267  aks4d1p3  43268  aks4d1p5  43270  aks4d1p6  43271  aks4d1p7d1  43272  aks4d1p7  43273  aks4d1p8  43277  aks4d1p9  43278  2np3bcnp1  43334  2ap1caineq  43335  aks6d1c7lem1  43370  aks6d1c7lem2  43371  aks6d1c7  43374  aks5lem6  43382  aks5lem8  43391  acos1half  43549  sn-0ne2  43597  3cubeslem2  43835  3cubeslem4  43839  jm2.23  44143  lt4addmuld  46461  stoweidlem11  47160  stoweidlem13  47162  stoweidlem26  47175  stoweidlem34  47183  stoweidlem42  47191  stoweidlem59  47208  stoweidlem62  47211  stoweid  47212  wallispilem4  47217  fourierdlem87  47342  smfmullem4  47943  modm2nep1  48581  modm1nep2  48583  fmtnoge3  48754  fmtnoprmfac2lem1  48790  31prm  48821  9fppr8  48974  fpprel2  48978  nfermltl8rev  48979  nfermltl2rev  48980  gbegt5  48998  gboge9  49001  sbgoldbwt  49014  sbgoldbst  49015  sbgoldbalt  49018  sbgoldbo  49024  nnsum3primes4  49025  nnsum4primes4  49026  nnsum4primesprm  49028  nnsum3primesgbe  49029  nnsum4primesgbe  49030  nnsum3primesle9  49031  nnsum4primesle9  49032  evengpop3  49035  evengpoap3  49036  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  cycl3grtri  49184  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb3  49271  usgrexmpl2nb4  49272  usgrexmpl2nb5  49273  usgrexmpl2trifr  49274  gpgusgralem  49293  gpg3nbgrvtx0  49313  gpg3kgrtriexlem1  49320  gpg3kgrtriexlem3  49322  gpg3kgrtriexlem4  49323  gpg3kgrtriexlem6  49325  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  pgrpgt2nabl  49617  ackval42  49947  sepfsepc  50181  veronesev3lem  51189  veronesev4lem  51190  veronesev5lem  51191  veronesev6lem  51192  veronesevrowd  51193  veroquadgsumlem  51197