Theorem 3re 12423

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 12406	. 2 ⊢ 3 = (2 + 1)
2		2re 12417	. . 3 ⊢ 2 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 3 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  2c2 12397  3c3 12398

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 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406

This theorem is used by:  4re  12427  2le3  12517  1lt3  12518  3lt4  12519  2lt4  12520  3lt5  12523  3lt6  12528  2lt6  12529  3lt7  12534  2lt7  12535  3lt8  12541  2lt8  12542  3lt9  12549  2lt9  12550  1le3  12557  3halfnz  12778  3lt10  12957  5eluz3  13010  uzuzle23  13011  uzuzle34  13013  uz3m2nn  13021  nn01to3  13068  3rp  13126  fz0to4untppr  13764  fz0to5un2tp  13765  expnass  14352  hashtpg  14630  hash3tpde  14638  01sqrexlem7  15415  sqrt9  15440  caucvgrlem  15840  bpoly4  16225  ef01bndlem  16352  sin01bnd  16353  cos2bnd  16356  sin01gt0  16358  cos01gt0  16359  egt2lt3  16374  rpnnen2lem3  16384  rpnnen2lem4  16385  rpnnen2lem9  16390  flodddiv4  16585  ge2nprmge4  16877  starvndxnmulrndx  17477  scandxnmulrndx  17489  vscandxnmulrndx  17494  ipndxnmulrndx  17505  tsetndxnmulrndx  17529  plendxnmulrndx  17543  dsndxnmulrndx  17562  slotsdifunifndx  17572  vitalilem4  25932  dveflem  26299  sincosq3sgn  26829  sincosq4sgn  26830  tangtx  26834  sincos6thpi  26844  pigt3  26846  pige3  26847  pige3ALT  26848  ang180lem2  27138  1cubrlem  27169  log2cnv  27272  log2tlbnd  27273  log2ub  27277  cxploglim2  27306  basellem5  27412  basellem9  27416  ppiublem1  27529  ppiub  27531  chtub  27539  bposlem2  27612  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  2lgslem3  27731  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  chto1ub  27803  dchrvmasumlem2  27825  dchrvmasumlema  27827  dchrvmasumiflem1  27828  mulog2sumlem2  27862  pntibndlem1  27916  pntibndlem2  27918  pntlemb  27924  pntlemk  27933  pntlemo  27934  fltoprmgt3  27996  istrkg3ld  28923  tgcgr4  28994  axlowdimlem16  29535  axlowdimlem17  29536  axlowdim  29539  usgrexmplef  29840  upgr4cycl4dv4e  30786  konigsbergiedgw  30849  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  konigsberglem4  30856  frgrogt3nreg  30998  friendshipgt3  30999  friendship  31000  ex-dif  31024  ex-in  31026  ex-fl  31048  ex-ceil  31049  ex-gcd  31058  threehalves  33481  iconstr  34398  2sqr3minply  34412  cos9thpiminplylem3  34416  cos9thpinconstrlem1  34421  prodfzo03  35232  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  cusgracyclt3v  35921  problem3  36432  problem5  36434  poimirlem9  38547  itg2addnclem2  38590  heiborlem5  38749  heiborlem6  38750  heiborlem7  38751  heiborlem8  38752  3lexlogpow5ineq2  43105  3lexlogpow5ineq4  43106  3lexlogpow5ineq3  43107  3lexlogpow2ineq1  43108  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1lem1  43112  aks4d1p1p3  43119  aks4d1p1p2  43120  aks4d1p1p4  43121  aks4d1p1p6  43123  aks4d1p1p5  43125  aks4d1p1  43126  aks4d1p2  43127  aks4d1p3  43128  aks4d1p5  43130  aks4d1p6  43131  aks4d1p7d1  43132  aks4d1p7  43133  aks4d1p8  43137  aks4d1p9  43138  2np3bcnp1  43194  2ap1caineq  43195  aks6d1c7lem1  43230  aks6d1c7lem2  43231  aks6d1c7  43234  aks5lem6  43242  aks5lem8  43251  acos1half  43409  sn-0ne2  43457  3cubeslem2  43695  3cubeslem4  43699  jm2.23  44002  lt4addmuld  46321  stoweidlem11  47020  stoweidlem13  47022  stoweidlem26  47035  stoweidlem34  47043  stoweidlem42  47051  stoweidlem59  47068  stoweidlem62  47071  stoweid  47072  wallispilem4  47077  fourierdlem87  47202  smfmullem4  47803  modm2nep1  48441  modm1nep2  48443  fmtnoge3  48614  fmtnoprmfac2lem1  48650  31prm  48681  9fppr8  48834  fpprel2  48838  nfermltl8rev  48839  nfermltl2rev  48840  gbegt5  48858  gboge9  48861  sbgoldbwt  48874  sbgoldbst  48875  sbgoldbalt  48878  sbgoldbo  48884  nnsum3primes4  48885  nnsum4primes4  48886  nnsum4primesprm  48888  nnsum3primesgbe  48889  nnsum4primesgbe  48890  nnsum3primesle9  48891  nnsum4primesle9  48892  evengpop3  48895  evengpoap3  48896  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  cycl3grtri  49044  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb3  49131  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  gpgusgralem  49153  gpg3nbgrvtx0  49173  gpg3kgrtriexlem1  49180  gpg3kgrtriexlem3  49182  gpg3kgrtriexlem4  49183  gpg3kgrtriexlem6  49185  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgrpgt2nabl  49477  ackval42  49807  sepfsepc  50035  veronesev3lem  50974  veronesev4lem  50975  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veroquadgsumlem  50982