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	⊢ ; 1 1 = ( ( 1 · ( ; 1 0 ↑ 1 ) ) + 1 )

Proof

Step	Hyp	Ref	Expression
1		dfdec10	⊢ ; 1 1 = ( ( ; 1 0 · 1 ) + 1 )
2		ax-1cn	⊢ 1 ∈ ℂ
3		10nn	⊢ ; 1 0 ∈ ℕ
4	3	nncni	⊢ ; 1 0 ∈ ℂ
5		exp1	⊢ ( ; 1 0 ∈ ℂ → ( ; 1 0 ↑ 1 ) = ; 1 0 )
6	4 5	ax-mp	⊢ ( ; 1 0 ↑ 1 ) = ; 1 0
7	6	eqcomi	⊢ ; 1 0 = ( ; 1 0 ↑ 1 )
8	7	oveq2i	⊢ ( 1 · ; 1 0 ) = ( 1 · ( ; 1 0 ↑ 1 ) )
9	2 4 8	mulcomli	⊢ ( ; 1 0 · 1 ) = ( 1 · ( ; 1 0 ↑ 1 ) )
10	9	oveq1i	⊢ ( ( ; 1 0 · 1 ) + 1 ) = ( ( 1 · ( ; 1 0 ↑ 1 ) ) + 1 )
11	1 10	eqtri	⊢ ; 1 1 = ( ( 1 · ( ; 1 0 ↑ 1 ) ) + 1 )