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

Metamath Proof Explorer

Theorem dfdec10

Description: Version of the definition of the "decimal constructor" using ; 1 0 instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion dfdec10 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )

Proof

Step Hyp Ref Expression
1 df-dec ⊢ 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )
2 9p1e10 ⊢ ( 9 + 1 ) = 1 0
3 2 oveq1i ⊢ ( ( 9 + 1 ) · 𝐴 ) = ( 1 0 · 𝐴 )
4 3 oveq1i ⊢ ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 ) = ( ( 1 0 · 𝐴 ) + 𝐵 )
5 1 4 eqtri ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )