Description: Define the number 9. (Contributed by NM, 27-May-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | df-9 | |- 9 = ( 8 + 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c9 | |- 9 |
|
1 | c8 | |- 8 |
|
2 | caddc | |- + |
|
3 | c1 | |- 1 |
|
4 | 1 3 2 | co | |- ( 8 + 1 ) |
5 | 0 4 | wceq | |- 9 = ( 8 + 1 ) |