Metamath Proof Explorer


Theorem 9t8e72

Description: 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 9t8e72 98=72

Proof

Step Hyp Ref Expression
1 9nn0 90
2 7nn0 70
3 df-8 8=7+1
4 9t7e63 97=63
5 6nn0 60
6 3nn0 30
7 eqid 63=63
8 6p1e7 6+1=7
9 2nn0 20
10 9cn 9
11 3cn 3
12 9p3e12 9+3=12
13 10 11 12 addcomli 3+9=12
14 5 6 1 7 8 9 13 decaddci 63+9=72
15 1 2 3 4 14 4t3lem 98=72