Theorem 3re 12338

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 12321	. 2 ⊢ 3 = (2 + 1)
2		2re 12332	. . 3 ⊢ 2 ∈ ℝ
3		1re 11225	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120  2c2 12312  3c3 12313

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321

This theorem is used by:  4re  12342  2le3  12432  1lt3  12433  3lt4  12434  2lt4  12435  3lt5  12438  3lt6  12443  2lt6  12444  3lt7  12449  2lt7  12450  3lt8  12456  2lt8  12457  3lt9  12464  2lt9  12465  1le3  12472  3halfnz  12693  3lt10  12872  5eluz3  12925  uzuzle23  12926  uzuzle34  12928  uz3m2nn  12936  nn01to3  12983  3rp  13040  fz0to4untppr  13677  fz0to5un2tp  13678  expnass  14264  hashtpg  14542  hash3tpde  14550  01sqrexlem7  15325  sqrt9  15350  caucvgrlem  15750  bpoly4  16137  ef01bndlem  16264  sin01bnd  16265  cos2bnd  16268  sin01gt0  16270  cos01gt0  16271  egt2lt3  16286  rpnnen2lem3  16296  rpnnen2lem4  16297  rpnnen2lem9  16302  flodddiv4  16497  ge2nprmge4  16784  starvndxnmulrndx  17383  scandxnmulrndx  17395  vscandxnmulrndx  17400  ipndxnmulrndx  17411  tsetndxnmulrndx  17435  plendxnmulrndx  17449  dsndxnmulrndx  17468  slotsdifunifndx  17478  vitalilem4  25823  dveflem  26191  sincosq3sgn  26718  sincosq4sgn  26719  tangtx  26723  sincos6thpi  26734  pigt3  26736  pige3  26737  pige3ALT  26738  ang180lem2  27028  1cubrlem  27059  log2cnv  27162  log2tlbnd  27163  log2ub  27167  cxploglim2  27196  basellem5  27302  basellem9  27306  ppiublem1  27419  ppiub  27421  chtub  27429  bposlem2  27502  bposlem3  27503  bposlem4  27504  bposlem5  27505  bposlem6  27506  bposlem8  27508  bposlem9  27509  lgsdir2lem1  27542  2lgslem3  27621  chebbnd1lem2  27687  chebbnd1lem3  27688  chebbnd1  27689  chto1ub  27693  dchrvmasumlem2  27715  dchrvmasumlema  27717  dchrvmasumiflem1  27718  mulog2sumlem2  27752  pntibndlem1  27806  pntibndlem2  27808  pntlemb  27814  pntlemk  27823  pntlemo  27824  istrkg3ld  28783  tgcgr4  28853  axlowdimlem16  29364  axlowdimlem17  29365  axlowdim  29368  usgrexmplef  29669  upgr4cycl4dv4e  30609  konigsbergiedgw  30672  konigsberglem1  30676  konigsberglem2  30677  konigsberglem3  30678  konigsberglem4  30679  frgrogt3nreg  30821  friendshipgt3  30822  friendship  30823  ex-dif  30847  ex-in  30849  ex-fl  30871  ex-ceil  30872  ex-gcd  30881  threehalves  33306  iconstr  34222  2sqr3minply  34236  cos9thpiminplylem3  34240  cos9thpinconstrlem1  34245  prodfzo03  35057  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  cusgracyclt3v  35687  problem3  36198  problem5  36200  poimirlem9  38339  itg2addnclem2  38382  heiborlem5  38526  heiborlem6  38527  heiborlem7  38528  heiborlem8  38529  3lexlogpow5ineq2  42882  3lexlogpow5ineq4  42883  3lexlogpow5ineq3  42884  3lexlogpow2ineq1  42885  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  aks4d1lem1  42889  aks4d1p1p3  42896  aks4d1p1p2  42897  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p5  42902  aks4d1p1  42903  aks4d1p2  42904  aks4d1p3  42905  aks4d1p5  42907  aks4d1p6  42908  aks4d1p7d1  42909  aks4d1p7  42910  aks4d1p8  42914  aks4d1p9  42915  2np3bcnp1  42971  2ap1caineq  42972  aks6d1c7lem1  43007  aks6d1c7lem2  43008  aks6d1c7  43011  aks5lem6  43019  aks5lem8  43028  acos1half  43179  sn-0ne2  43227  3cubeslem2  43476  3cubeslem4  43480  jm2.23  43783  lt4addmuld  46085  stoweidlem11  46785  stoweidlem13  46787  stoweidlem26  46800  stoweidlem34  46808  stoweidlem42  46816  stoweidlem59  46833  stoweidlem62  46836  stoweid  46837  wallispilem4  46842  fourierdlem87  46967  smfmullem4  47568  modm2nep1  48169  modm1nep2  48171  fmtnoge3  48342  fmtnoprmfac2lem1  48378  31prm  48409  9fppr8  48562  fpprel2  48566  nfermltl8rev  48567  nfermltl2rev  48568  gbegt5  48586  gboge9  48589  sbgoldbwt  48602  sbgoldbst  48603  sbgoldbalt  48606  sbgoldbo  48612  nnsum3primes4  48613  nnsum4primes4  48614  nnsum4primesprm  48616  nnsum3primesgbe  48617  nnsum4primesgbe  48618  nnsum3primesle9  48619  nnsum4primesle9  48620  evengpop3  48623  evengpoap3  48624  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  wtgoldbnnsum4prm  48627  bgoldbnnsum3prm  48629  cycl3grtri  48772  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb3  48859  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862  gpgusgralem  48881  gpg3nbgrvtx0  48901  gpg3kgrtriexlem1  48908  gpg3kgrtriexlem3  48910  gpg3kgrtriexlem4  48911  gpg3kgrtriexlem6  48913  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgrpgt2nabl  49205  ackval42  49535  sepfsepc  49765