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	|- A e. NN0
	decaddm10.b	|- B e. NN0
Assertion	decaddm10	|- ( ; A 0 + ; B 0 ) = ; ( A + B ) 0

Proof

Step	Hyp	Ref	Expression
1		decaddm10.a	|- A e. NN0
2		decaddm10.b	|- B e. NN0
3		0nn0	|- 0 e. NN0
4		eqid	|- ; A 0 = ; A 0
5		eqid	|- ; B 0 = ; B 0
6		eqid	|- ( A + B ) = ( A + B )
7		00id	|- ( 0 + 0 ) = 0
8	1 3 2 3 4 5 6 7	decadd	|- ( ; A 0 + ; B 0 ) = ; ( A + B ) 0