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

Theorem 3re 12234
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 12218 . 2 3 = (2 + 1)
2 2re 12228 . . 3 2 ∈ ℝ
3 1re 11156 . . 3 1 ∈ ℝ
42, 3readdcli 11171 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2834 1 3 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cr 11051  1c1 11053   + caddc 11055  2c2 12209  3c3 12210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-i2m1 11120  ax-1ne0 11121  ax-rrecex 11124  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-2 12217  df-3 12218
This theorem is referenced by:  4re  12238  3ne0  12260  4pos  12261  1lt3  12327  3lt4  12328  2lt4  12329  3lt5  12332  3lt6  12337  2lt6  12338  3lt7  12343  2lt7  12344  3lt8  12350  2lt8  12351  3lt9  12358  2lt9  12359  1le3  12366  3halfnz  12583  3lt10  12756  2lt10  12757  uzuzle23  12815  uz3m2nn  12817  nn01to3  12867  3rp  12922  fz0to4untppr  13545  expnass  14113  hashtpg  14385  01sqrexlem7  15134  sqrt9  15159  caucvgrlem  15558  bpoly4  15943  ef01bndlem  16067  sin01bnd  16068  cos2bnd  16071  sin01gt0  16073  cos01gt0  16074  egt2lt3  16089  rpnnen2lem3  16099  rpnnen2lem4  16100  rpnnen2lem9  16105  flodddiv4  16296  ge2nprmge4  16578  starvndxnmulrndx  17188  scandxnmulrndx  17200  vscandxnmulrndx  17205  ipndxnmulrndx  17216  tsetndxnmulrndx  17240  plendxnmulrndx  17254  dsndxnmulrndx  17273  slotsdifunifndx  17283  cnfldfunALTOLD  20813  matscaOLD  21766  matvscaOLD  21768  vitalilem4  24978  dveflem  25346  sincosq3sgn  25860  sincosq4sgn  25861  tangtx  25865  sincos6thpi  25875  pigt3  25877  pige3  25878  pige3ALT  25879  ang180lem2  26163  1cubrlem  26194  log2cnv  26297  log2tlbnd  26298  log2ub  26302  cxploglim2  26331  basellem5  26437  basellem9  26441  ppiublem1  26553  ppiub  26555  chtub  26563  bposlem2  26636  bposlem3  26637  bposlem4  26638  bposlem5  26639  bposlem6  26640  bposlem8  26642  bposlem9  26643  lgsdir2lem1  26676  2lgslem3  26755  chebbnd1lem2  26821  chebbnd1lem3  26822  chebbnd1  26823  chto1ub  26827  dchrvmasumlem2  26849  dchrvmasumlema  26851  dchrvmasumiflem1  26852  mulog2sumlem2  26886  pntibndlem1  26940  pntibndlem2  26942  pntlemb  26948  pntlemk  26957  pntlemo  26958  istrkg3ld  27406  tgcgr4  27476  axlowdimlem16  27909  axlowdimlem17  27910  axlowdim  27913  usgrexmplef  28210  upgr4cycl4dv4e  29132  konigsbergiedgw  29195  konigsberglem1  29199  konigsberglem2  29200  konigsberglem3  29201  konigsberglem4  29202  frgrogt3nreg  29344  friendshipgt3  29345  friendship  29346  ex-dif  29370  ex-in  29372  ex-fl  29394  ex-ceil  29395  ex-gcd  29404  threehalves  31774  resvmulrOLD  32134  prodfzo03  33219  hgt750lem  33267  hgt750lem2  33268  hgt750leme  33274  cusgracyclt3v  33753  problem3  34258  problem5  34260  poimirlem9  36090  itg2addnclem2  36133  heiborlem5  36277  heiborlem6  36278  heiborlem7  36279  heiborlem8  36280  3lexlogpow5ineq2  40515  3lexlogpow5ineq4  40516  3lexlogpow5ineq3  40517  3lexlogpow2ineq1  40518  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1lem1  40522  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8  40547  aks4d1p9  40548  2np3bcnp1  40555  2ap1caineq  40556  2xp3dxp2ge1d  40617  acos1half  40625  sn-0ne2  40878  3cubeslem2  41011  3cubeslem4  41015  jm2.23  41323  jm2.20nn  41324  mnringscadOLD  42510  mnringvscadOLD  42512  lt4addmuld  43547  stoweidlem11  44259  stoweidlem13  44261  stoweidlem26  44274  stoweidlem34  44282  stoweidlem42  44290  stoweidlem59  44307  stoweidlem62  44310  stoweid  44311  wallispilem4  44316  fourierdlem87  44441  smfmullem4  45042  fmtnoge3  45729  fmtnoprmfac2lem1  45765  31prm  45796  9fppr8  45936  fpprel2  45940  nfermltl8rev  45941  nfermltl2rev  45942  gbegt5  45960  gboge9  45963  sbgoldbwt  45976  sbgoldbst  45977  sbgoldbalt  45980  sbgoldbo  45986  nnsum3primes4  45987  nnsum4primes4  45988  nnsum4primesprm  45990  nnsum3primesgbe  45991  nnsum4primesgbe  45992  nnsum3primesle9  45993  nnsum4primesle9  45994  evengpop3  45997  evengpoap3  45998  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  wtgoldbnnsum4prm  46001  bgoldbnnsum3prm  46003  pgrpgt2nabl  46449  ackval42  46789  sepfsepc  46967
  Copyright terms: Public domain W3C validator