Theorem 9t11e99

Description: 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Assertion	9t11e99	$$⊢9\cdot 11=99$$

Proof

Step	Hyp	Ref	Expression
1		9cn	$$⊢9\in ℂ$$
2		10nn0	$$⊢10\in {\mathbb{N}}_0$$
3	2	nn0cni	$$⊢10\in ℂ$$
4		ax-1cn	$$⊢1\in ℂ$$
5	3 4	mulcli	$$⊢10\cdot 1\in ℂ$$
6	1 5 4	adddii	$$⊢9\left(10\cdot 1+1\right)=910\cdot 1+9\cdot 1$$
7	3	mulid1i	$$⊢10\cdot 1=10$$
8	7	oveq2i	$$⊢910\cdot 1=9\cdot 10$$
9	1 3	mulcomi	$$⊢9\cdot 10=10\cdot 9$$
10	8 9	eqtri	$$⊢910\cdot 1=10\cdot 9$$
11	1	mulid1i	$$⊢9\cdot 1=9$$
12	10 11	oveq12i	$$⊢910\cdot 1+9\cdot 1=10\cdot 9+9$$
13	6 12	eqtri	$$⊢9\left(10\cdot 1+1\right)=10\cdot 9+9$$
14		dfdec10	$$⊢11=10\cdot 1+1$$
15	14	oveq2i	$$⊢9\cdot 11=9\left(10\cdot 1+1\right)$$
16		dfdec10	$$⊢99=10\cdot 9+9$$
17	13 15 16	3eqtr4i	$$⊢9\cdot 11=99$$