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 |