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$$

Proof

Step	Hyp	Ref	Expression
1		dfdec10	$$⊢11=10\cdot 1+1$$
2		ax-1cn	$$⊢1\in ℂ$$
3		10nn	$$⊢10\in \mathbb{N}$$
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$$