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

Theorem 3re 10941
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 10927 . 2 3 = (2 + 1)
2 2re 10937 . . 3 2 ∈ ℝ
3 1re 9895 . . 3 1 ∈ ℝ
42, 3readdcli 9909 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2683 1 3 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  (class class class)co 6527  cr 9791  1c1 9793   + caddc 9795  2c2 10917  3c3 10918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926  df-3 10927
This theorem is referenced by:  3cn  10942  4re  10944  3ne0  10962  4pos  10963  1lt3  11043  3lt4  11044  2lt4  11045  3lt5  11048  3lt6  11053  2lt6  11054  3lt7  11059  2lt7  11060  3lt8  11066  2lt8  11067  3lt9  11074  2lt9  11075  3lt10OLD  11083  2lt10OLD  11084  1le3  11091  3halfnz  11288  3lt10  11511  2lt10  11512  uzuzle23  11561  uz3m2nn  11563  nn01to3  11613  3rp  11670  fz0to4untppr  12266  expnass  12787  hashtpg  13071  sqrlem7  13783  sqrt9  13808  caucvgrlem  14197  caurcvgr  14198  bpoly4  14575  ef01bndlem  14699  sin01bnd  14700  cos2bnd  14703  sin01gt0  14705  cos01gt0  14706  egt2lt3  14719  rpnnen2lem3  14730  rpnnen2lem4  14731  rpnnen2lem9  14736  flodddiv4  14921  matsca  19982  matvsca  19983  vitalilem4  23103  dveflem  23463  sincosq3sgn  23973  sincosq4sgn  23974  tangtx  23978  sincos6thpi  23988  pige3  23990  ang180lem2  24257  1cubrlem  24285  log2cnv  24388  log2tlbnd  24389  log2ub  24393  cxploglim2  24422  basellem5  24528  basellem9  24532  cht3  24616  ppiublem1  24644  ppiub  24646  chtub  24654  bposlem2  24727  bposlem3  24728  bposlem4  24729  bposlem5  24730  bposlem6  24731  bposlem8  24733  bposlem9  24734  lgsdir2lem1  24767  2lgslem3  24846  chebbnd1lem2  24876  chebbnd1lem3  24877  chebbnd1  24878  chto1ub  24882  dchrvmasumlem2  24904  dchrvmasumlema  24906  dchrvmasumiflem1  24907  mulog2sumlem2  24941  pntibndlem1  24995  pntibndlem2  24997  pntlemb  25003  pntlemk  25012  pntlemo  25013  istrkg3ld  25077  axlowdimlem8  25547  axlowdimlem9  25548  axlowdimlem16  25555  axlowdimlem17  25556  axlowdim  25559  usgraex3elv  25693  constr3pthlem3  25951  4cycl4v4e  25960  4cycl4dv4e  25962  konigsberg  26280  extwwlkfablem2  26371  numclwlk1lem2f1  26387  frgraogt3nreg  26413  friendshipgt3  26414  friendship  26415  ex-dif  26438  ex-in  26440  ex-1st  26459  ex-2nd  26460  ex-fl  26462  ex-ceil  26463  ex-gcd  26472  resvmulr  28972  problem3  30621  problem5  30623  pigt3  32368  poimirlem9  32384  itg2addnclem2  32428  heiborlem5  32580  heiborlem6  32581  heiborlem7  32582  heiborlem8  32583  jm2.23  36377  jm2.20nn  36378  lt4addmuld  38257  stoweidlem11  38701  stoweidlem13  38703  stoweidlem26  38716  stoweidlem34  38724  stoweidlem42  38732  stoweidlem59  38749  stoweidlem62  38752  stoweid  38753  wallispilem4  38758  fourierdlem87  38883  smfmullem4  39476  fmtnoge3  39778  fmtnoprmfac2lem1  39814  31prm  39848  gbegt5  39981  gboage9  39984  bgoldbwt  39997  bgoldbst  39998  sgoldbalt  40001  nnsum3primes4  40002  nnsum4primes4  40003  nnsum4primesprm  40005  nnsum3primesgbe  40006  nnsum4primesgbe  40007  nnsum3primesle9  40008  nnsum4primesle9  40009  evengpop3  40012  evengpoap3  40013  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  wtgoldbnnsum4prm  40016  bgoldbnnsum3prm  40018  upgr4cycl4dv4e  41347  konigsbergiedgw  41411  konigsbergiedgwOLD  41412  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419  konigsberglem4  41420  av-numclwlk1lem2f1  41519  av-frgraogt3nreg  41546  av-friendshipgt3  41547  av-friendship  41548  pgrpgt2nabl  41936
  Copyright terms: Public domain W3C validator