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

Theorem 3re 11132
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 11118 . 2 3 = (2 + 1)
2 2re 11128 . . 3 2 ∈ ℝ
3 1re 10077 . . 3 1 ∈ ℝ
42, 3readdcli 10091 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2726 1 3 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  (class class class)co 6690  cr 9973  1c1 9975   + caddc 9977  2c2 11108  3c3 11109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118
This theorem is referenced by:  3cn  11133  4re  11135  3ne0  11153  4pos  11154  1lt3  11234  3lt4  11235  2lt4  11236  3lt5  11239  3lt6  11244  2lt6  11245  3lt7  11250  2lt7  11251  3lt8  11257  2lt8  11258  3lt9  11265  2lt9  11266  3lt10OLD  11274  2lt10OLD  11275  1le3  11282  3halfnz  11494  3lt10  11717  2lt10  11718  uzuzle23  11767  uz3m2nn  11769  nn01to3  11819  3rp  11876  fz0to4untppr  12481  expnass  13010  hashtpg  13305  sqrlem7  14033  sqrt9  14058  caucvgrlem  14447  caurcvgr  14448  bpoly4  14834  ef01bndlem  14958  sin01bnd  14959  cos2bnd  14962  sin01gt0  14964  cos01gt0  14965  egt2lt3  14978  rpnnen2lem3  14989  rpnnen2lem4  14990  rpnnen2lem9  14995  flodddiv4  15184  cnfldfun  19806  matsca  20269  matvsca  20270  vitalilem4  23425  dveflem  23787  sincosq3sgn  24297  sincosq4sgn  24298  tangtx  24302  sincos6thpi  24312  pige3  24314  ang180lem2  24585  1cubrlem  24613  log2cnv  24716  log2tlbnd  24717  log2ub  24721  cxploglim2  24750  basellem5  24856  basellem9  24860  cht3  24944  ppiublem1  24972  ppiub  24974  chtub  24982  bposlem2  25055  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem1  25095  2lgslem3  25174  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  chto1ub  25210  dchrvmasumlem2  25232  dchrvmasumlema  25234  dchrvmasumiflem1  25235  mulog2sumlem2  25269  pntibndlem1  25323  pntibndlem2  25325  pntlemb  25331  pntlemk  25340  pntlemo  25341  istrkg3ld  25405  axlowdimlem8  25874  axlowdimlem9  25875  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  usgrexmplef  26196  upgr4cycl4dv4e  27163  konigsbergiedgw  27226  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem4  27233  frgrogt3nreg  27384  friendshipgt3  27385  friendship  27386  ex-dif  27410  ex-in  27412  ex-1st  27431  ex-2nd  27432  ex-fl  27434  ex-ceil  27435  ex-gcd  27444  threehalves  29751  resvmulr  29963  prodfzo03  30809  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  problem3  31687  problem5  31689  pigt3  33532  poimirlem9  33548  itg2addnclem2  33592  heiborlem5  33744  heiborlem6  33745  heiborlem7  33746  heiborlem8  33747  jm2.23  37880  jm2.20nn  37881  lt4addmuld  39834  stoweidlem11  40546  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  stoweidlem42  40577  stoweidlem59  40594  stoweidlem62  40597  stoweid  40598  wallispilem4  40603  fourierdlem87  40728  smfmullem4  41322  fmtnoge3  41767  fmtnoprmfac2lem1  41803  31prm  41837  gbegt5  41974  gboge9  41977  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbalt  41994  sbgoldbo  42000  nnsum3primes4  42001  nnsum4primes4  42002  nnsum4primesprm  42004  nnsum3primesgbe  42005  nnsum4primesgbe  42006  nnsum3primesle9  42007  nnsum4primesle9  42008  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  pgrpgt2nabl  42472
  Copyright terms: Public domain W3C validator