Theorem 3re 12205

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 12189	. 2 ⊢ 3 = (2 + 1)
2		2re 12199	. . 3 ⊢ 2 ∈ ℝ
3		1re 11112	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11127	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005  1c1 11007   + caddc 11009  2c2 12180  3c3 12181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188  df-3 12189

This theorem is referenced by:  4re  12209  4pos  12232  1lt3  12293  3lt4  12294  2lt4  12295  3lt5  12298  3lt6  12303  2lt6  12304  3lt7  12309  2lt7  12310  3lt8  12316  2lt8  12317  3lt9  12324  2lt9  12325  1le3  12332  3halfnz  12552  3lt10  12725  2lt10  12726  5eluz3  12781  uzuzle23  12782  uzuzle34  12784  uz3m2nn  12792  nn01to3  12839  3rp  12896  fz0to4untppr  13530  fz0to5un2tp  13531  expnass  14115  hashtpg  14392  hash3tpde  14400  01sqrexlem7  15155  sqrt9  15180  caucvgrlem  15580  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos2bnd  16097  sin01gt0  16099  cos01gt0  16100  egt2lt3  16115  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  flodddiv4  16326  ge2nprmge4  16612  starvndxnmulrndx  17210  scandxnmulrndx  17222  vscandxnmulrndx  17227  ipndxnmulrndx  17238  tsetndxnmulrndx  17262  plendxnmulrndx  17276  dsndxnmulrndx  17295  slotsdifunifndx  17305  vitalilem4  25539  dveflem  25910  sincosq3sgn  26436  sincosq4sgn  26437  tangtx  26441  sincos6thpi  26452  pigt3  26454  pige3  26455  pige3ALT  26456  ang180lem2  26747  1cubrlem  26778  log2cnv  26881  log2tlbnd  26882  log2ub  26886  cxploglim2  26916  basellem5  27022  basellem9  27026  ppiublem1  27140  ppiub  27142  chtub  27150  bposlem2  27223  bposlem3  27224  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem8  27229  bposlem9  27230  lgsdir2lem1  27263  2lgslem3  27342  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chto1ub  27414  dchrvmasumlem2  27436  dchrvmasumlema  27438  dchrvmasumiflem1  27439  mulog2sumlem2  27473  pntibndlem1  27527  pntibndlem2  27529  pntlemb  27535  pntlemk  27544  pntlemo  27545  istrkg3ld  28439  tgcgr4  28509  axlowdimlem16  28935  axlowdimlem17  28936  axlowdim  28939  usgrexmplef  29237  upgr4cycl4dv4e  30165  konigsbergiedgw  30228  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  konigsberglem4  30235  frgrogt3nreg  30377  friendshipgt3  30378  friendship  30379  ex-dif  30403  ex-in  30405  ex-fl  30427  ex-ceil  30428  ex-gcd  30437  threehalves  32895  iconstr  33779  2sqr3minply  33793  cos9thpiminplylem3  33797  cos9thpinconstrlem1  33802  prodfzo03  34616  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  cusgracyclt3v  35200  problem3  35711  problem5  35713  poimirlem9  37679  itg2addnclem2  37722  heiborlem5  37865  heiborlem6  37866  heiborlem7  37867  heiborlem8  37868  3lexlogpow5ineq2  42158  3lexlogpow5ineq4  42159  3lexlogpow5ineq3  42160  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1lem1  42165  aks4d1p1p3  42172  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p5  42178  aks4d1p1  42179  aks4d1p2  42180  aks4d1p3  42181  aks4d1p5  42183  aks4d1p6  42184  aks4d1p7d1  42185  aks4d1p7  42186  aks4d1p8  42190  aks4d1p9  42191  2np3bcnp1  42247  2ap1caineq  42248  aks6d1c7lem1  42283  aks6d1c7lem2  42284  aks6d1c7  42287  aks5lem6  42295  aks5lem8  42304  acos1half  42461  sn-0ne2  42509  3cubeslem2  42788  3cubeslem4  42792  jm2.23  43099  jm2.20nn  43100  lt4addmuld  45417  stoweidlem11  46119  stoweidlem13  46121  stoweidlem26  46134  stoweidlem34  46142  stoweidlem42  46150  stoweidlem59  46167  stoweidlem62  46170  stoweid  46171  wallispilem4  46176  fourierdlem87  46301  smfmullem4  46902  modm2nep1  47476  modm1nep2  47478  fmtnoge3  47640  fmtnoprmfac2lem1  47676  31prm  47707  9fppr8  47847  fpprel2  47851  nfermltl8rev  47852  nfermltl2rev  47853  gbegt5  47871  gboge9  47874  sbgoldbwt  47887  sbgoldbst  47888  sbgoldbalt  47891  sbgoldbo  47897  nnsum3primes4  47898  nnsum4primes4  47899  nnsum4primesprm  47901  nnsum3primesgbe  47902  nnsum4primesgbe  47903  nnsum3primesle9  47904  nnsum4primesle9  47905  evengpop3  47908  evengpoap3  47909  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  cycl3grtri  48057  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb3  48144  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  usgrexmpl2trifr  48147  gpgusgralem  48166  gpg3nbgrvtx0  48186  gpg3kgrtriexlem1  48193  gpg3kgrtriexlem3  48195  gpg3kgrtriexlem4  48196  gpg3kgrtriexlem6  48198  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgrpgt2nabl  48476  ackval42  48807  sepfsepc  49038