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$

Step	Hyp	Ref	Expression
1		9cn	$⊢ 9 \in ℂ$
2		10nn0	$⊢ 10 \in ℕ_{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 (10 \cdot 1 + 1) = 9 10 \cdot 1 + 9 \cdot 1$
7	3	mulridi	$⊢ 10 \cdot 1 = 10$
8	7	oveq2i	$⊢ 9 10 \cdot 1 = 9 \cdot 10$
9	1 3	mulcomi	$⊢ 9 \cdot 10 = 10 \cdot 9$
10	8 9	eqtri	$⊢ 9 10 \cdot 1 = 10 \cdot 9$
11	1	mulridi	$⊢ 9 \cdot 1 = 9$
12	10 11	oveq12i	$⊢ 9 10 \cdot 1 + 9 \cdot 1 = 10 \cdot 9 + 9$
13	6 12	eqtri	$⊢ 9 (10 \cdot 1 + 1) = 10 \cdot 9 + 9$
14		dfdec10	$⊢ 11 = 10 \cdot 1 + 1$
15	14	oveq2i	$⊢ 9 \cdot 11 = 9 (10 \cdot 1 + 1)$
16		dfdec10	$⊢ 99 = 10 \cdot 9 + 9$
17	13 15 16	3eqtr4i	$⊢ 9 \cdot 11 = 99$

Metamath Proof Explorer