Theorem 8t7e56

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

	Ref	Expression
Assertion	8t7e56	⊢ ( 8 · 7 ) = ; 5 6

Proof

Step	Hyp	Ref	Expression
1		8nn0	⊢ 8 ∈ ℕ0
2		6nn0	⊢ 6 ∈ ℕ0
3		df-7	⊢ 7 = ( 6 + 1 )
4		8t6e48	⊢ ( 8 · 6 ) = ; 4 8
5		4nn0	⊢ 4 ∈ ℕ0
6		eqid	⊢ ; 4 8 = ; 4 8
7		4p1e5	⊢ ( 4 + 1 ) = 5
8		8p8e16	⊢ ( 8 + 8 ) = ; 1 6
9	5 1 1 6 7 2 8	decaddci	⊢ ( ; 4 8 + 8 ) = ; 5 6
10	1 2 3 4 9	4t3lem	⊢ ( 8 · 7 ) = ; 5 6