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

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 12228 . 2 6 = (5 + 1)
2 5re 12248 . . 3 5 ∈ ℝ
3 1re 11163 . . 3 1 ∈ ℝ
42, 3readdcli 11178 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2830 1 6 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7361  cr 11058  1c1 11060   + caddc 11062  5c5 12219  6c6 12220
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 2704  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-i2m1 11127  ax-1ne0 11128  ax-rrecex 11131  ax-cnre 11132
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 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-ov 7364  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228
This theorem is referenced by:  7re  12254  7pos  12272  4lt6  12343  3lt6  12344  2lt6  12345  1lt6  12346  6lt7  12347  5lt7  12348  6lt8  12354  5lt8  12355  6lt9  12362  5lt9  12363  8th4div3  12381  halfpm6th  12382  div4p1lem1div2  12416  6lt10  12760  5lt10  12761  5recm6rec  12770  bpoly2  15948  bpoly3  15949  efi4p  16027  resin4p  16028  recos4p  16029  ef01bndlem  16074  sin01bnd  16075  cos01bnd  16076  slotsdifipndx  17224  slotstnscsi  17249  plendxnvscandx  17263  slotsdnscsi  17281  lt6abl  19680  sralemOLD  20684  sravscaOLD  20694  zlmlemOLD  20941  sincos6thpi  25895  pigt3  25897  basellem5  26457  basellem8  26460  basellem9  26461  ppiublem1  26573  ppiublem2  26574  ppiub  26575  chtub  26583  bposlem6  26660  bposlem8  26662  slotsinbpsd  27432  slotslnbpsd  27433  ex-res  29434  zlmdsOLD  32608  zlmtsetOLD  32610  hgt750lemd  33325  hgt750lem2  33329  hgt750leme  33335  problem4  34320  problem5  34321  gbegt5  46043  gbowgt5  46044  gbowge7  46045  gboge9  46046  sbgoldbwt  46059  sgoldbeven3prm  46065  mogoldbb  46067  sbgoldbo  46069  nnsum3primesle9  46076  nnsum4primesodd  46078  wtgoldbnnsum4prm  46084  bgoldbnnsum3prm  46086  pgrple2abl  46531
  Copyright terms: Public domain W3C validator