This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1t10e1p1e11

Description: 11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	1t10e1p1e11	$⊢ 11 = 1 10^{1} + 1$

Step	Hyp	Ref	Expression
1		dfdec10	$⊢ 11 = 10 \cdot 1 + 1$
2		ax-1cn	$⊢ 1 \in ℂ$
3		10nn	$⊢ 10 \in ℕ$
4	3	nncni	$⊢ 10 \in ℂ$
5		exp1	$⊢ 10 \in ℂ \to 10^{1} = 10$
6	4 5	ax-mp	$⊢ 10^{1} = 10$
7	6	eqcomi	$⊢ 10 = 10^{1}$
8	7	oveq2i	$⊢ 1 \cdot 10 = 1 10^{1}$
9	2 4 8	mulcomli	$⊢ 10 \cdot 1 = 1 10^{1}$
10	9	oveq1i	$⊢ 10 \cdot 1 + 1 = 1 10^{1} + 1$
11	1 10	eqtri	$⊢ 11 = 1 10^{1} + 1$