Theorem 9t7e63

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

	Ref	Expression
Assertion	9t7e63	$$⊢9\cdot 7=63$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		df-7	$$⊢7=6+1$$
4		9t6e54	$$⊢9\cdot 6=54$$
5		5nn0	$$⊢5\in {\mathbb{N}}_0$$
6		4nn0	$$⊢4\in {\mathbb{N}}_0$$
7		eqid	$$⊢54=54$$
8		5p1e6	$$⊢5+1=6$$
9		3nn0	$$⊢3\in {\mathbb{N}}_0$$
10	1	nn0cni	$$⊢9\in ℂ$$
11	6	nn0cni	$$⊢4\in ℂ$$
12		9p4e13	$$⊢9+4=13$$
13	10 11 12	addcomli	$$⊢4+9=13$$
14	5 6 1 7 8 9 13	decaddci	$$⊢54+9=63$$
15	1 2 3 4 14	4t3lem	$$⊢9\cdot 7=63$$