Theorem 9t6e54

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

	Ref	Expression
Assertion	9t6e54	$$⊢9\cdot 6=54$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3		df-6	$$⊢6=5+1$$
4		9t5e45	$$⊢9\cdot 5=45$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6		eqid	$$⊢45=45$$
7		4p1e5	$$⊢4+1=5$$
8	1	nn0cni	$$⊢9\in ℂ$$
9	2	nn0cni	$$⊢5\in ℂ$$
10		9p5e14	$$⊢9+5=14$$
11	8 9 10	addcomli	$$⊢5+9=14$$
12	5 2 1 6 7 5 11	decaddci	$$⊢45+9=54$$
13	1 2 3 4 12	4t3lem	$$⊢9\cdot 6=54$$