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 ( 1 0 + 𝐴 ) = 1 𝐴

Proof

Step Hyp Ref Expression
1 dfdec10 ⊢ 1 𝐴 = ( ( 1 0 · 1 ) + 𝐴 )
2 10nn ⊢ 1 0 ∈ ℕ
3 2 nncni ⊢ 1 0 ∈ ℂ
4 3 mulid1i ⊢ ( 1 0 · 1 ) = 1 0
5 4 oveq1i ⊢ ( ( 1 0 · 1 ) + 𝐴 ) = ( 1 0 + 𝐴 )
6 1 5 eqtr2i ⊢ ( 1 0 + 𝐴 ) = 1 𝐴