Theorem 3re 12321

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 12304	. 2 ⊢ 3 = (2 + 1)
2		2re 12315	. . 3 ⊢ 2 ∈ ℝ
3		1re 11208	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11224	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2865	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11099  1c1 11101   + caddc 11103  2c2 12295  3c3 12296

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 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-i2m1 11168  ax-1ne0 11169  ax-rrecex 11172  ax-cnre 11173

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 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304

This theorem is referenced by:  4re  12325  2le3  12415  1lt3  12416  3lt4  12417  2lt4  12418  3lt5  12421  3lt6  12426  2lt6  12427  3lt7  12432  2lt7  12433  3lt8  12439  2lt8  12440  3lt9  12447  2lt9  12448  1le3  12455  3halfnz  12675  3lt10  12854  5eluz3  12907  uzuzle23  12908  uzuzle34  12910  uz3m2nn  12918  nn01to3  12965  3rp  13022  fz0to4untppr  13658  fz0to5un2tp  13659  expnass  14244  hashtpg  14522  hash3tpde  14530  01sqrexlem7  15299  sqrt9  15324  caucvgrlem  15724  bpoly4  16113  ef01bndlem  16240  sin01bnd  16241  cos2bnd  16244  sin01gt0  16246  cos01gt0  16247  egt2lt3  16262  rpnnen2lem3  16272  rpnnen2lem4  16273  rpnnen2lem9  16278  flodddiv4  16473  ge2nprmge4  16760  starvndxnmulrndx  17359  scandxnmulrndx  17371  vscandxnmulrndx  17376  ipndxnmulrndx  17387  tsetndxnmulrndx  17411  plendxnmulrndx  17425  dsndxnmulrndx  17444  slotsdifunifndx  17454  vitalilem4  25739  dveflem  26107  sincosq3sgn  26631  sincosq4sgn  26632  tangtx  26636  sincos6thpi  26647  pigt3  26649  pige3  26650  pige3ALT  26651  ang180lem2  26941  1cubrlem  26972  log2cnv  27075  log2tlbnd  27076  log2ub  27080  cxploglim2  27109  basellem5  27215  basellem9  27219  ppiublem1  27332  ppiub  27334  chtub  27342  bposlem2  27415  bposlem3  27416  bposlem4  27417  bposlem5  27418  bposlem6  27419  bposlem8  27421  bposlem9  27422  lgsdir2lem1  27455  2lgslem3  27534  chebbnd1lem2  27600  chebbnd1lem3  27601  chebbnd1  27602  chto1ub  27606  dchrvmasumlem2  27628  dchrvmasumlema  27630  dchrvmasumiflem1  27631  mulog2sumlem2  27665  pntibndlem1  27719  pntibndlem2  27721  pntlemb  27727  pntlemk  27736  pntlemo  27737  istrkg3ld  28696  tgcgr4  28766  axlowdimlem16  29248  axlowdimlem17  29249  axlowdim  29252  usgrexmplef  29550  upgr4cycl4dv4e  30477  konigsbergiedgw  30540  konigsberglem1  30544  konigsberglem2  30545  konigsberglem3  30546  konigsberglem4  30547  frgrogt3nreg  30689  friendshipgt3  30690  friendship  30691  ex-dif  30715  ex-in  30717  ex-fl  30739  ex-ceil  30740  ex-gcd  30749  threehalves  33175  iconstr  34101  2sqr3minply  34115  cos9thpiminplylem3  34119  cos9thpinconstrlem1  34124  prodfzo03  34935  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  cusgracyclt3v  35547  problem3  36058  problem5  36060  poimirlem9  38168  itg2addnclem2  38211  heiborlem5  38354  heiborlem6  38355  heiborlem7  38356  heiborlem8  38357  3lexlogpow5ineq2  42712  3lexlogpow5ineq4  42713  3lexlogpow5ineq3  42714  3lexlogpow2ineq1  42715  3lexlogpow2ineq2  42716  3lexlogpow5ineq5  42717  aks4d1lem1  42719  aks4d1p1p3  42726  aks4d1p1p2  42727  aks4d1p1p4  42728  aks4d1p1p6  42730  aks4d1p1p5  42732  aks4d1p1  42733  aks4d1p2  42734  aks4d1p3  42735  aks4d1p5  42737  aks4d1p6  42738  aks4d1p7d1  42739  aks4d1p7  42740  aks4d1p8  42744  aks4d1p9  42745  2np3bcnp1  42801  2ap1caineq  42802  aks6d1c7lem1  42837  aks6d1c7lem2  42838  aks6d1c7  42841  aks5lem6  42849  aks5lem8  42858  acos1half  43009  sn-0ne2  43057  3cubeslem2  43308  3cubeslem4  43312  jm2.23  43615  lt4addmuld  45917  stoweidlem11  46617  stoweidlem13  46619  stoweidlem26  46632  stoweidlem34  46640  stoweidlem42  46648  stoweidlem59  46665  stoweidlem62  46668  stoweid  46669  wallispilem4  46674  fourierdlem87  46799  smfmullem4  47400  modm2nep1  47998  modm1nep2  48000  fmtnoge3  48171  fmtnoprmfac2lem1  48207  31prm  48238  9fppr8  48391  fpprel2  48395  nfermltl8rev  48396  nfermltl2rev  48397  gbegt5  48415  gboge9  48418  sbgoldbwt  48431  sbgoldbst  48432  sbgoldbalt  48435  sbgoldbo  48441  nnsum3primes4  48442  nnsum4primes4  48443  nnsum4primesprm  48445  nnsum3primesgbe  48446  nnsum4primesgbe  48447  nnsum3primesle9  48448  nnsum4primesle9  48449  evengpop3  48452  evengpoap3  48453  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  wtgoldbnnsum4prm  48456  bgoldbnnsum3prm  48458  cycl3grtri  48601  usgrexmpl1lem  48675  usgrexmpl2lem  48680  usgrexmpl2nb3  48688  usgrexmpl2nb4  48689  usgrexmpl2nb5  48690  usgrexmpl2trifr  48691  gpgusgralem  48710  gpg3nbgrvtx0  48730  gpg3kgrtriexlem1  48737  gpg3kgrtriexlem3  48739  gpg3kgrtriexlem4  48740  gpg3kgrtriexlem6  48742  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  pgrpgt2nabl  49031  ackval42  49361  sepfsepc  49591