Metamath Proof Explorer

Theorem deceq1

Description: Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion deceq1 
|- ( A = B -> ; A C = ; B C )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( A = B -> ( ( 9 + 1 ) x. A ) = ( ( 9 + 1 ) x. B ) )
2 1 oveq1d 
 |-  ( A = B -> ( ( ( 9 + 1 ) x. A ) + C ) = ( ( ( 9 + 1 ) x. B ) + C ) )
3 df-dec 
 |-  ; A C = ( ( ( 9 + 1 ) x. A ) + C )
4 df-dec 
 |-  ; B C = ( ( ( 9 + 1 ) x. B ) + C )
5 2 3 4 3eqtr4g 
 |-  ( A = B -> ; A C = ; B C )