Theorem difelfzle

Description: The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)

	Ref	Expression
Assertion	difelfzle	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
2		elfznn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
3		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
4		nn0z	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
5		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
6	3 4 5	syl2anr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
7	6	adantr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
8		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
9		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
10		subge0	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ ( 𝑀 − 𝐾 ) ↔ 𝐾 ≤ 𝑀 ) )
11	8 9 10	syl2anr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 − 𝐾 ) ↔ 𝐾 ≤ 𝑀 ) )
12	11	biimpar	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → 0 ≤ ( 𝑀 − 𝐾 ) )
13	7 12	jca	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
14	13	exp31	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑀 → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) ) ) )
15	1 2 14	syl2im	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ≤ 𝑀 → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) ) ) )
16	15	3imp	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
17		elnn0z	⊢ ( ( 𝑀 − 𝐾 ) ∈ ℕ0 ↔ ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
18	16 17	sylibr	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ℕ0 )
19		elfz3nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
20	19	3ad2ant1	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → 𝑁 ∈ ℕ0 )
21		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
22	8	3ad2ant1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
23		resubcl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 − 𝐾 ) ∈ ℝ )
24	22 9 23	syl2an	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ∈ ℝ )
25	22	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
26		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
27	26	3ad2ant2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
28	27	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
29		nn0ge0	⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
30	29	adantl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ 𝐾 )
31		subge02	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ 𝐾 ↔ ( 𝑀 − 𝐾 ) ≤ 𝑀 ) )
32	22 9 31	syl2an	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 0 ≤ 𝐾 ↔ ( 𝑀 − 𝐾 ) ≤ 𝑀 ) )
33	30 32	mpbid	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ≤ 𝑀 )
34		simpl3	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ≤ 𝑁 )
35	24 25 28 33 34	letrd	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 )
36	35	ex	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
37	21 36	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
38	1 37	syl5com	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
39	38	a1dd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ≤ 𝑀 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) ) )
40	39	3imp	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 )
41		elfz2nn0	⊢ ( ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝑀 − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
42	18 20 40 41	syl3anbrc	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) )