Theorem 9t4e36

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

	Ref	Expression
Assertion	9t4e36	$$⊢9\cdot 4=36$$

Proof

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