Description: 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 9t6e54 | |- ( 9 x. 6 ) = ; 5 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 9nn0 | |- 9 e. NN0 |
|
2 | 5nn0 | |- 5 e. NN0 |
|
3 | df-6 | |- 6 = ( 5 + 1 ) |
|
4 | 9t5e45 | |- ( 9 x. 5 ) = ; 4 5 |
|
5 | 4nn0 | |- 4 e. NN0 |
|
6 | eqid | |- ; 4 5 = ; 4 5 |
|
7 | 4p1e5 | |- ( 4 + 1 ) = 5 |
|
8 | 1 | nn0cni | |- 9 e. CC |
9 | 2 | nn0cni | |- 5 e. CC |
10 | 9p5e14 | |- ( 9 + 5 ) = ; 1 4 |
|
11 | 8 9 10 | addcomli | |- ( 5 + 9 ) = ; 1 4 |
12 | 5 2 1 6 7 5 11 | decaddci | |- ( ; 4 5 + 9 ) = ; 5 4 |
13 | 1 2 3 4 12 | 4t3lem | |- ( 9 x. 6 ) = ; 5 4 |