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

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 10623 . 2
2 5re 10639 . . 3
3 1re 9616 . . 3
42, 3readdcli 9630 . 2
51, 4eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cr 9512  1c1 9514   caddc 9516  5c5 10613  6c6 10614
This theorem is referenced by:  6cn  10642  7re  10643  7pos  10660  4lt6  10738  3lt6  10739  2lt6  10740  1lt6  10741  6lt7  10742  5lt7  10743  6lt8  10749  5lt8  10750  6lt9  10757  5lt9  10758  6lt10  10766  5lt10  10767  8th4div3  10784  halfpm6th  10785  efi4p  13872  resin4p  13873  recos4p  13874  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  lt6abl  16897  sralem  17823  sravsca  17828  zlmlem  18554  sincos6thpi  22908  basellem5  23358  basellem8  23361  basellem9  23362  ppiublem1  23477  ppiublem2  23478  ppiub  23479  chtub  23487  bposlem6  23564  bposlem8  23566  ex-res  25162  zlmds  27945  zlmtset  27946  problem4  29022  problem5  29023  5recm6rec  29114  bpoly2  29819  bpoly3  29820  3lcm2e6  31219  pgrple2abl  32958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623
  Copyright terms: Public domain W3C validator