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\in {\mathbb{N}}_0$$
	decaddm10.b	$$⊢B\in {\mathbb{N}}_0$$
Assertion	decaddm10	Could not format assertion : No typesetting found for |- ( ; A 0 + ; B 0 ) = ; ( A + B ) 0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decaddm10.a	$$⊢A\in {\mathbb{N}}_0$$
2		decaddm10.b	$$⊢B\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		eqid	Could not format ; A 0 = ; A 0 : No typesetting found for |- ; A 0 = ; A 0 with typecode |-
5		eqid	Could not format ; B 0 = ; B 0 : No typesetting found for |- ; B 0 = ; B 0 with typecode |-
6		eqid	$$⊢A+B=A+B$$
7		00id	$$⊢0+0=0$$
8	1 3 2 3 4 5 6 7	decadd	Could not format ( ; A 0 + ; B 0 ) = ; ( A + B ) 0 : No typesetting found for |- ( ; A 0 + ; B 0 ) = ; ( A + B ) 0 with typecode |-