Theorem 8t8e64

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

	Ref	Expression
Assertion	8t8e64	$$⊢8\cdot 8=64$$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		7nn0	$$⊢7\in {\mathbb{N}}_0$$
3		df-8	$$⊢8=7+1$$
4		8t7e56	$$⊢8\cdot 7=56$$
5		5nn0	$$⊢5\in {\mathbb{N}}_0$$
6		6nn0	$$⊢6\in {\mathbb{N}}_0$$
7		eqid	$$⊢56=56$$
8		5p1e6	$$⊢5+1=6$$
9		4nn0	$$⊢4\in {\mathbb{N}}_0$$
10	1	nn0cni	$$⊢8\in ℂ$$
11	6	nn0cni	$$⊢6\in ℂ$$
12		8p6e14	$$⊢8+6=14$$
13	10 11 12	addcomli	$$⊢6+8=14$$
14	5 6 1 7 8 9 13	decaddci	$$⊢56+8=64$$
15	1 2 3 4 14	4t3lem	$$⊢8\cdot 8=64$$