Theorem fz0addge0

Description: The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018)

	Ref	Expression
Assertion	fz0addge0	$$⊢\left(A\in \left(0\dots M\right)\wedge B\in \left(0\dots N\right)\right)\to 0\le A+B$$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$$⊢A\in \left(0\dots M\right)\to A\in {\mathbb{N}}_0$$
2		elfznn0	$$⊢B\in \left(0\dots N\right)\to B\in {\mathbb{N}}_0$$
3	1 2	anim12i	$$⊢\left(A\in \left(0\dots M\right)\wedge B\in \left(0\dots N\right)\right)\to \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)$$
4		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
5		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
6	4 5	anim12i	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A\in ℝ\wedge B\in ℝ\right)$$
7		nn0ge0	$$⊢A\in {\mathbb{N}}_0\to 0\le A$$
8		nn0ge0	$$⊢B\in {\mathbb{N}}_0\to 0\le B$$
9	7 8	anim12i	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(0\le A\wedge 0\le B\right)$$
10	6 9	jca	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(0\le A\wedge 0\le B\right)\right)$$
11		addge0	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(0\le A\wedge 0\le B\right)\right)\to 0\le A+B$$
12	3 10 11	3syl	$$⊢\left(A\in \left(0\dots M\right)\wedge B\in \left(0\dots N\right)\right)\to 0\le A+B$$