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 + A ) = ; 1 A

Proof

Step Hyp Ref Expression
1 dfdec10 
 |-  ; 1 A = ( ( ; 1 0 x. 1 ) + A )
2 10nn 
 |-  ; 1 0 e. NN
3 2 nncni 
 |-  ; 1 0 e. CC
4 3 mulid1i 
 |-  ( ; 1 0 x. 1 ) = ; 1 0
5 4 oveq1i 
 |-  ( ( ; 1 0 x. 1 ) + A ) = ( ; 1 0 + A )
6 1 5 eqtr2i 
 |-  ( ; 1 0 + A ) = ; 1 A