Metamath Proof Explorer


Theorem 8re

Description: The number 8 is real. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion 8re
|- 8 e. RR

Proof

Step Hyp Ref Expression
1 df-8
 |-  8 = ( 7 + 1 )
2 7re
 |-  7 e. RR
3 1re
 |-  1 e. RR
4 2 3 readdcli
 |-  ( 7 + 1 ) e. RR
5 1 4 eqeltri
 |-  8 e. RR