Theorem dec10p

Description: Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Assertion	dec10p	Could not format assertion : No typesetting found for |- ( ; 1 0 + A ) = ; 1 A with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfdec10	Could not format ; 1 A = ( ( ; 1 0 x. 1 ) + A ) : No typesetting found for |- ; 1 A = ( ( ; 1 0 x. 1 ) + A ) with typecode |-
2		10nn	$$⊢10\in \mathbb{N}$$
3	2	nncni	$$⊢10\in ℂ$$
4	3	mulid1i	$$⊢10\cdot 1=10$$
5	4	oveq1i	$$⊢10\cdot 1+A=10+A$$
6	1 5	eqtr2i	Could not format ( ; 1 0 + A ) = ; 1 A : No typesetting found for |- ( ; 1 0 + A ) = ; 1 A with typecode |-