Description: 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 9t8e72 | |- ( 9 x. 8 ) = ; 7 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 9nn0 | |- 9 e. NN0 |
|
2 | 7nn0 | |- 7 e. NN0 |
|
3 | df-8 | |- 8 = ( 7 + 1 ) |
|
4 | 9t7e63 | |- ( 9 x. 7 ) = ; 6 3 |
|
5 | 6nn0 | |- 6 e. NN0 |
|
6 | 3nn0 | |- 3 e. NN0 |
|
7 | eqid | |- ; 6 3 = ; 6 3 |
|
8 | 6p1e7 | |- ( 6 + 1 ) = 7 |
|
9 | 2nn0 | |- 2 e. NN0 |
|
10 | 9cn | |- 9 e. CC |
|
11 | 3cn | |- 3 e. CC |
|
12 | 9p3e12 | |- ( 9 + 3 ) = ; 1 2 |
|
13 | 10 11 12 | addcomli | |- ( 3 + 9 ) = ; 1 2 |
14 | 5 6 1 7 8 9 13 | decaddci | |- ( ; 6 3 + 9 ) = ; 7 2 |
15 | 1 2 3 4 14 | 4t3lem | |- ( 9 x. 8 ) = ; 7 2 |