Theorem 8t4e32

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

	Ref	Expression
Assertion	8t4e32	⊢ ( 8 · 4 ) = ; 3 2

Proof

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