Theorem 9t9e81

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

	Ref	Expression
Assertion	9t9e81	$$⊢9\cdot 9=81$$

Proof

Step	Hyp	Ref	Expression
1		9nn0	$$⊢9\in {\mathbb{N}}_0$$
2		8nn0	$$⊢8\in {\mathbb{N}}_0$$
3		df-9	$$⊢9=8+1$$
4		9t8e72	$$⊢9\cdot 8=72$$
5		7nn0	$$⊢7\in {\mathbb{N}}_0$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		eqid	$$⊢72=72$$
8		7p1e8	$$⊢7+1=8$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		9cn	$$⊢9\in ℂ$$
11		2cn	$$⊢2\in ℂ$$
12		9p2e11	$$⊢9+2=11$$
13	10 11 12	addcomli	$$⊢2+9=11$$
14	5 6 1 7 8 9 13	decaddci	$$⊢72+9=81$$
15	1 2 3 4 14	4t3lem	$$⊢9\cdot 9=81$$