MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3re Structured version   Visualization version   GIF version

Theorem 3re 11709
Description: The number 3 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
3re 3 ∈ ℝ

Proof of Theorem 3re
StepHypRef Expression
1 df-3 11693 . 2 3 = (2 + 1)
2 2re 11703 . . 3 2 ∈ ℝ
3 1re 10633 . . 3 1 ∈ ℝ
42, 3readdcli 10648 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2913 1 3 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7151  cr 10528  1c1 10530   + caddc 10532  2c2 11684  3c3 11685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-i2m1 10597  ax-1ne0 10598  ax-rrecex 10601  ax-cnre 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154  df-2 11692  df-3 11693
This theorem is referenced by:  4re  11713  3ne0  11735  4pos  11736  1lt3  11802  3lt4  11803  2lt4  11804  3lt5  11807  3lt6  11812  2lt6  11813  3lt7  11818  2lt7  11819  3lt8  11825  2lt8  11826  3lt9  11833  2lt9  11834  1le3  11841  3halfnz  12053  3lt10  12227  2lt10  12228  uzuzle23  12281  uz3m2nn  12283  nn01to3  12333  3rp  12388  fz0to4untppr  13003  expnass  13563  hashtpg  13836  sqrlem7  14601  sqrt9  14626  caucvgrlem  15022  bpoly4  15405  ef01bndlem  15529  sin01bnd  15530  cos2bnd  15533  sin01gt0  15535  cos01gt0  15536  egt2lt3  15551  rpnnen2lem3  15561  rpnnen2lem4  15562  rpnnen2lem9  15567  flodddiv4  15756  ge2nprmge4  16037  cnfldfun  20473  matsca  20940  matvsca  20941  vitalilem4  24127  dveflem  24491  sincosq3sgn  25001  sincosq4sgn  25002  tangtx  25006  sincos6thpi  25016  pigt3  25018  pige3  25019  pige3ALT  25020  ang180lem2  25301  1cubrlem  25332  log2cnv  25436  log2tlbnd  25437  log2ub  25441  cxploglim2  25470  basellem5  25576  basellem9  25580  ppiublem1  25692  ppiub  25694  chtub  25702  bposlem2  25775  bposlem3  25776  bposlem4  25777  bposlem5  25778  bposlem6  25779  bposlem8  25781  bposlem9  25782  lgsdir2lem1  25815  2lgslem3  25894  chebbnd1lem2  25960  chebbnd1lem3  25961  chebbnd1  25962  chto1ub  25966  dchrvmasumlem2  25988  dchrvmasumlema  25990  dchrvmasumiflem1  25991  mulog2sumlem2  26025  pntibndlem1  26079  pntibndlem2  26081  pntlemb  26087  pntlemk  26096  pntlemo  26097  istrkg3ld  26161  tgcgr4  26231  axlowdimlem16  26657  axlowdimlem17  26658  axlowdim  26661  usgrexmplef  26955  upgr4cycl4dv4e  27878  konigsbergiedgw  27941  konigsberglem1  27945  konigsberglem2  27946  konigsberglem3  27947  konigsberglem4  27948  frgrogt3nreg  28090  friendshipgt3  28091  friendship  28092  ex-dif  28116  ex-in  28118  ex-fl  28140  ex-ceil  28141  ex-gcd  28150  threehalves  30505  resvmulr  30822  prodfzo03  31760  hgt750lem  31808  hgt750lem2  31809  hgt750leme  31815  cusgracyclt3v  32287  problem3  32794  problem5  32796  poimirlem9  34768  itg2addnclem2  34811  heiborlem5  34961  heiborlem6  34962  heiborlem7  34963  heiborlem8  34964  sn-0ne2  39099  3cubeslem2  39143  3cubeslem4  39147  jm2.23  39454  jm2.20nn  39455  lt4addmuld  41434  stoweidlem11  42158  stoweidlem13  42160  stoweidlem26  42173  stoweidlem34  42181  stoweidlem42  42189  stoweidlem59  42206  stoweidlem62  42209  stoweid  42210  wallispilem4  42215  fourierdlem87  42340  smfmullem4  42931  fmtnoge3  43520  fmtnoprmfac2lem1  43556  31prm  43588  9fppr8  43730  fpprel2  43734  nfermltl8rev  43735  nfermltl2rev  43736  gbegt5  43754  gboge9  43757  sbgoldbwt  43770  sbgoldbst  43771  sbgoldbalt  43774  sbgoldbo  43780  nnsum3primes4  43781  nnsum4primes4  43782  nnsum4primesprm  43784  nnsum3primesgbe  43785  nnsum4primesgbe  43786  nnsum3primesle9  43787  nnsum4primesle9  43788  evengpop3  43791  evengpoap3  43792  nnsum4primeseven  43793  nnsum4primesevenALTV  43794  wtgoldbnnsum4prm  43795  bgoldbnnsum3prm  43797  pgrpgt2nabl  44242
  Copyright terms: Public domain W3C validator