Theorem fz0addcom

Description: The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018) (Revised by Alexander van der Vekens, 9-Jun-2018)

	Ref	Expression
Assertion	fz0addcom	$$⊢\left(A\in \left(0\dots N\right)\wedge B\in \left(0\dots N\right)\right)\to A+B=B+A$$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$$⊢A\in \left(0\dots N\right)\to A\in {\mathbb{N}}_0$$
2	1	nn0cnd	$$⊢A\in \left(0\dots N\right)\to A\in ℂ$$
3		elfznn0	$$⊢B\in \left(0\dots N\right)\to B\in {\mathbb{N}}_0$$
4	3	nn0cnd	$$⊢B\in \left(0\dots N\right)\to B\in ℂ$$
5		addcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$
6	2 4 5	syl2an	$$⊢\left(A\in \left(0\dots N\right)\wedge B\in \left(0\dots N\right)\right)\to A+B=B+A$$