Theorem 9t3e27

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

	Ref	Expression
Assertion	9t3e27	$$⊢9\cdot 3=27$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		df-3	$$⊢3=2+1$$
4		9t2e18	$$⊢9\cdot 2=18$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		eqid	$$⊢18=18$$
8		1p1e2	$$⊢1+1=2$$
9		7nn0	$$⊢7\in {\mathbb{N}}_0$$
10	1	nn0cni	$$⊢9\in ℂ$$
11	6	nn0cni	$$⊢8\in ℂ$$
12		9p8e17	$$⊢9+8=17$$
13	10 11 12	addcomli	$$⊢8+9=17$$
14	5 6 1 7 8 9 13	decaddci	$$⊢18+9=27$$
15	1 2 3 4 14	4t3lem	$$⊢9\cdot 3=27$$