Theorem 7t5e35

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

	Ref	Expression
Assertion	7t5e35	$$⊢7\cdot 5=35$$

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		df-5	$$⊢5=4+1$$
4		7t4e28	$$⊢7\cdot 4=28$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		eqid	$$⊢28=28$$
8		2p1e3	$$⊢2+1=3$$
9		5nn0	$$⊢5\in {\mathbb{N}}_0$$
10		8p7e15	$$⊢8+7=15$$
11	5 6 1 7 8 9 10	decaddci	$$⊢28+7=35$$
12	1 2 3 4 11	4t3lem	$$⊢7\cdot 5=35$$