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

Theorem 6re 11719
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 11696 . 2 6 = (5 + 1)
2 5re 11716 . . 3 5 ∈ ℝ
3 1re 10634 . . 3 1 ∈ ℝ
42, 3readdcli 10649 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2889 1 6 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cr 10529  1c1 10531   + caddc 10533  5c5 11687  6c6 11688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696
This theorem is referenced by:  7re  11722  7pos  11740  4lt6  11811  3lt6  11812  2lt6  11813  1lt6  11814  6lt7  11815  5lt7  11816  6lt8  11822  5lt8  11823  6lt9  11830  5lt9  11831  8th4div3  11849  halfpm6th  11850  div4p1lem1div2  11884  6lt10  12224  5lt10  12225  5recm6rec  12234  bpoly2  15406  bpoly3  15407  efi4p  15485  resin4p  15486  recos4p  15487  ef01bndlem  15532  sin01bnd  15533  cos01bnd  15534  lt6abl  19011  sralem  19945  sravsca  19950  zlmlem  20213  sincos6thpi  25111  pigt3  25113  basellem5  25673  basellem8  25676  basellem9  25677  ppiublem1  25789  ppiublem2  25790  ppiub  25791  chtub  25799  bposlem6  25876  bposlem8  25878  ex-res  28229  zlmds  31313  zlmtset  31314  hgt750lemd  32027  hgt750lem2  32031  hgt750leme  32037  problem4  33019  problem5  33020  gbegt5  44266  gbowgt5  44267  gbowge7  44268  gboge9  44269  sbgoldbwt  44282  sgoldbeven3prm  44288  mogoldbb  44290  sbgoldbo  44292  nnsum3primesle9  44299  nnsum4primesodd  44301  wtgoldbnnsum4prm  44307  bgoldbnnsum3prm  44309  pgrple2abl  44754
  Copyright terms: Public domain W3C validator