Theorem 9t8e72

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

	Ref	Expression
Assertion	9t8e72	⊢ ( 9 · 8 ) = ; 7 2

Proof

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