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	⊢ ( ( 𝐴 ∈ ( 0 ... 𝑀 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elfznn0	⊢ ( 𝐴 ∈ ( 0 ... 𝑀 ) → 𝐴 ∈ ℕ0 )
2		elfznn0	⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → 𝐵 ∈ ℕ0 )
3	1 2	anim12i	⊢ ( ( 𝐴 ∈ ( 0 ... 𝑀 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) )
4		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
5		nn0re	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
6	4 5	anim12i	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
7		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
8		nn0ge0	⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
9	7 8	anim12i	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) )
10	6 9	jca	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) )
11		addge0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )
12	3 10 11	3syl	⊢ ( ( 𝐴 ∈ ( 0 ... 𝑀 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )