Theorem 7t7e49

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

	Ref	Expression
Assertion	7t7e49	$$⊢7\cdot 7=49$$

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		df-7	$$⊢7=6+1$$
4		7t6e42	$$⊢7\cdot 6=42$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		eqid	$$⊢42=42$$
8		7cn	$$⊢7\in ℂ$$
9		2cn	$$⊢2\in ℂ$$
10		7p2e9	$$⊢7+2=9$$
11	8 9 10	addcomli	$$⊢2+7=9$$
12	5 6 1 7 11	decaddi	$$⊢42+7=49$$
13	1 2 3 4 12	4t3lem	$$⊢7\cdot 7=49$$