Theorem 9t3e27

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

	Ref	Expression
Assertion	9t3e27	⊢ ( 9 · 3 ) = ; 2 7

Proof

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