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 x. ( ; 1 0 ^ 1 ) ) + 1 )

Proof

Step	Hyp	Ref	Expression
1		dfdec10	|- ; 1 1 = ( ( ; 1 0 x. 1 ) + 1 )
2		ax-1cn	|- 1 e. CC
3		10nn	|- ; 1 0 e. NN
4	3	nncni	|- ; 1 0 e. CC
5		exp1	|- ( ; 1 0 e. CC -> ( ; 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 x. ; 1 0 ) = ( 1 x. ( ; 1 0 ^ 1 ) )
9	2 4 8	mulcomli	|- ( ; 1 0 x. 1 ) = ( 1 x. ( ; 1 0 ^ 1 ) )
10	9	oveq1i	|- ( ( ; 1 0 x. 1 ) + 1 ) = ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 )
11	1 10	eqtri	|- ; 1 1 = ( ( 1 x. ( ; 1 0 ^ 1 ) ) + 1 )