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

Theorem 6re 11303
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 11285 . 2 6 = (5 + 1)
2 5re 11301 . . 3 5 ∈ ℝ
3 1re 10241 . . 3 1 ∈ ℝ
42, 3readdcli 10255 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2846 1 6 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  (class class class)co 6793  cr 10137  1c1 10139   + caddc 10141  5c5 11275  6c6 11276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-i2m1 10206  ax-1ne0 10207  ax-rrecex 10210  ax-cnre 10211
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285
This theorem is referenced by:  6cn  11304  7re  11305  7pos  11322  4lt6  11407  3lt6  11408  2lt6  11409  1lt6  11410  6lt7  11411  5lt7  11412  6lt8  11418  5lt8  11419  6lt9  11426  5lt9  11427  6lt10OLD  11435  5lt10OLD  11436  8th4div3  11454  halfpm6th  11455  div4p1lem1div2  11489  6lt10  11877  5lt10  11878  5recm6rec  11887  bpoly2  14994  bpoly3  14995  efi4p  15073  resin4p  15074  recos4p  15075  ef01bndlem  15120  sin01bnd  15121  cos01bnd  15122  lt6abl  18503  sralem  19392  sravsca  19397  zlmlem  20080  sincos6thpi  24488  basellem5  25032  basellem8  25035  basellem9  25036  ppiublem1  25148  ppiublem2  25149  ppiub  25150  chtub  25158  bposlem6  25235  bposlem8  25237  ex-res  27640  zlmds  30348  zlmtset  30349  hgt750lemd  31066  hgt750lem2  31070  hgt750leme  31076  problem4  31900  problem5  31901  pigt3  33735  gbegt5  42177  gbowgt5  42178  gbowge7  42179  gboge9  42180  sbgoldbwt  42193  sgoldbeven3prm  42199  mogoldbb  42201  sbgoldbo  42203  nnsum3primesle9  42210  nnsum4primesodd  42212  wtgoldbnnsum4prm  42218  bgoldbnnsum3prm  42220  pgrple2abl  42674
  Copyright terms: Public domain W3C validator