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