Theorem 9t11e99OLD

Description: Obsolete version of 9t11e99 as of 10-Jun-2026. (Contributed by AV, 14-Jun-2021) (Revised by AV, 6-Sep-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	9t11e99OLD	$$⊢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	mulridi	$$⊢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	mulridi	$$⊢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$$