Theorem 6t4e24

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

	Ref	Expression
Assertion	6t4e24	⊢ ( 6 · 4 ) = ; 2 4

Proof

Step	Hyp	Ref	Expression
1		6nn0	⊢ 6 ∈ ℕ0
2		3nn0	⊢ 3 ∈ ℕ0
3		df-4	⊢ 4 = ( 3 + 1 )
4		6t3e18	⊢ ( 6 · 3 ) = ; 1 8
5		1nn0	⊢ 1 ∈ ℕ0
6		8nn0	⊢ 8 ∈ ℕ0
7		eqid	⊢ ; 1 8 = ; 1 8
8		1p1e2	⊢ ( 1 + 1 ) = 2
9		4nn0	⊢ 4 ∈ ℕ0
10		8p6e14	⊢ ( 8 + 6 ) = ; 1 4
11	5 6 1 7 8 9 10	decaddci	⊢ ( ; 1 8 + 6 ) = ; 2 4
12	1 2 3 4 11	4t3lem	⊢ ( 6 · 4 ) = ; 2 4