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

Metamath Proof Explorer

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

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 ℕ$
3	2	nncni	$⊢ 10 \in ℂ$
4	3	mulridi	$⊢ 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 \|-