Metamath Proof Explorer


Theorem decaddm10

Description: The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021)

Ref Expression
Hypotheses decaddm10.a 𝐴 ∈ ℕ0
decaddm10.b 𝐵 ∈ ℕ0
Assertion decaddm10 ( 𝐴 0 + 𝐵 0 ) = ( 𝐴 + 𝐵 ) 0

Proof

Step Hyp Ref Expression
1 decaddm10.a 𝐴 ∈ ℕ0
2 decaddm10.b 𝐵 ∈ ℕ0
3 0nn0 0 ∈ ℕ0
4 eqid 𝐴 0 = 𝐴 0
5 eqid 𝐵 0 = 𝐵 0
6 eqid ( 𝐴 + 𝐵 ) = ( 𝐴 + 𝐵 )
7 00id ( 0 + 0 ) = 0
8 1 3 2 3 4 5 6 7 decadd ( 𝐴 0 + 𝐵 0 ) = ( 𝐴 + 𝐵 ) 0