Theorem 9t9e81

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

	Ref	Expression
Assertion	9t9e81	⊢ ( 9 · 9 ) = ; 8 1

Proof

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