Theorem 7t6e42

Description: 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	7t6e42	$$⊢7\cdot 6=42$$

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3		df-6	$$⊢6=5+1$$
4		7t5e35	$$⊢7\cdot 5=35$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		eqid	$$⊢35=35$$
7		3p1e4	$$⊢3+1=4$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9	1	nn0cni	$$⊢7\in ℂ$$
10	2	nn0cni	$$⊢5\in ℂ$$
11		7p5e12	$$⊢7+5=12$$
12	9 10 11	addcomli	$$⊢5+7=12$$
13	5 2 1 6 7 8 12	decaddci	$$⊢35+7=42$$
14	1 2 3 4 13	4t3lem	$$⊢7\cdot 6=42$$