Theorem 9t8e72

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

	Ref	Expression
Assertion	9t8e72	$$⊢9\cdot 8=72$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		7nn0	$$⊢7\in {\mathbb{N}}_0$$
3		df-8	$$⊢8=7+1$$
4		9t7e63	$$⊢9\cdot 7=63$$
5		6nn0	$$⊢6\in {\mathbb{N}}_0$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7		eqid	$$⊢63=63$$
8		6p1e7	$$⊢6+1=7$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10		9cn	$$⊢9\in ℂ$$
11		3cn	$$⊢3\in ℂ$$
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	$$⊢9\cdot 8=72$$