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

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

Proof of Theorem 8re
StepHypRef Expression
1 df-8 9015 . 2 8 = (7 + 1)
2 7re 9033 . . 3 7 ∈ ℝ
3 1re 7987 . . 3 1 ∈ ℝ
42, 3readdcli 8001 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2262 1 8 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2160  (class class class)co 5897  cr 7841  1c1 7843   + caddc 7845  7c7 9006  8c8 9007
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 7936  ax-addrcl 7939
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9009  df-3 9010  df-4 9011  df-5 9012  df-6 9013  df-7 9014  df-8 9015
This theorem is referenced by:  8cn  9036  9re  9037  9pos  9054  6lt8  9141  5lt8  9142  4lt8  9143  3lt8  9144  2lt8  9145  1lt8  9146  8lt9  9147  7lt9  9148  8th4div3  9169  8lt10  9546  7lt10  9547  ef01bndlem  11799  cos2bnd  11803  slotstnscsi  12709  slotsdnscsi  12733  2lgsoddprmlem1  14931  2lgsoddprmlem2  14932  2lgsoddprmlem3a  14933  2lgsoddprmlem3b  14934  2lgsoddprmlem3c  14935  2lgsoddprmlem3d  14936
  Copyright terms: Public domain W3C validator