ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  6re Unicode version

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 9017 . 2  |-  6  =  ( 5  +  1 )
2 5re 9033 . . 3  |-  5  e.  RR
3 1re 7991 . . 3  |-  1  e.  RR
42, 3readdcli 8005 . 2  |-  ( 5  +  1 )  e.  RR
51, 4eqeltri 2262 1  |-  6  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 2160  (class class class)co 5900   RRcr 7845   1c1 7847    + caddc 7849   5c5 9008   6c6 9009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1re 7940  ax-addrcl 7943
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9013  df-3 9014  df-4 9015  df-5 9016  df-6 9017
This theorem is referenced by:  6cn  9036  7re  9037  7pos  9056  4lt6  9134  3lt6  9135  2lt6  9136  1lt6  9137  6lt7  9138  5lt7  9139  6lt8  9145  5lt8  9146  6lt9  9153  5lt9  9154  8th4div3  9173  halfpm6th  9174  div4p1lem1div2  9207  6lt10  9552  5lt10  9553  5recm6rec  9562  efi4p  11766  resin4p  11767  recos4p  11768  ef01bndlem  11805  sin01bnd  11806  cos01bnd  11807  slotsdifipndx  12697  slotstnscsi  12717  plendxnvscandx  12731  slotsdnscsi  12741  sincos6thpi  14748  pigt3  14750
  Copyright terms: Public domain W3C validator