Theorem 9t4e36

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

	Ref	Expression
Assertion	9t4e36	|- ( 9 x. 4 ) = ; 3 6

Proof

Step	Hyp	Ref	Expression
1		9nn0	|- 9 e. NN0
2		3nn0	|- 3 e. NN0
3		df-4	|- 4 = ( 3 + 1 )
4		9t3e27	|- ( 9 x. 3 ) = ; 2 7
5		2nn0	|- 2 e. NN0
6		7nn0	|- 7 e. NN0
7		eqid	|- ; 2 7 = ; 2 7
8		2p1e3	|- ( 2 + 1 ) = 3
9		6nn0	|- 6 e. NN0
10	1	nn0cni	|- 9 e. CC
11	6	nn0cni	|- 7 e. CC
12		9p7e16	|- ( 9 + 7 ) = ; 1 6
13	10 11 12	addcomli	|- ( 7 + 9 ) = ; 1 6
14	5 6 1 7 8 9 13	decaddci	|- ( ; 2 7 + 9 ) = ; 3 6
15	1 2 3 4 14	4t3lem	|- ( 9 x. 4 ) = ; 3 6