Theorem 8t8e64

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

	Ref	Expression
Assertion	8t8e64	⊢ ( 8 · 8 ) = ; 6 4

Proof

Step	Hyp	Ref	Expression
1		8nn0	⊢ 8 ∈ ℕ0
2		7nn0	⊢ 7 ∈ ℕ0
3		df-8	⊢ 8 = ( 7 + 1 )
4		8t7e56	⊢ ( 8 · 7 ) = ; 5 6
5		5nn0	⊢ 5 ∈ ℕ0
6		6nn0	⊢ 6 ∈ ℕ0
7		eqid	⊢ ; 5 6 = ; 5 6
8		5p1e6	⊢ ( 5 + 1 ) = 6
9		4nn0	⊢ 4 ∈ ℕ0
10	1	nn0cni	⊢ 8 ∈ ℂ
11	6	nn0cni	⊢ 6 ∈ ℂ
12		8p6e14	⊢ ( 8 + 6 ) = ; 1 4
13	10 11 12	addcomli	⊢ ( 6 + 8 ) = ; 1 4
14	5 6 1 7 8 9 13	decaddci	⊢ ( ; 5 6 + 8 ) = ; 6 4
15	1 2 3 4 14	4t3lem	⊢ ( 8 · 8 ) = ; 6 4