Theorem fz0fzdiffz0

Description: The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		fz0fzelfz0	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
2		elfzle1	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝐾 )
3	2	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝐾 )
4	3	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑀 ≤ 𝐾 )
5		elfznn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
6	5	adantr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℕ0 )
7		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
8		nn0sub	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
9	6 7 8	syl2anr	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
10	4 9	mpbid	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
11		elfz3nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
12	11	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
13		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
14		elfz2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
15		zsubcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
16	15	zred	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
17	16	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
18	17	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
19		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
20	19	3ad2ant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ )
21		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
22	21	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℝ )
23	18 20 22	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
24	23	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
25	24	adantr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
26		nn0ge0	⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
27	26	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ 𝑀 )
28		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
29		subge02	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ 𝑀 ↔ ( 𝐾 − 𝑀 ) ≤ 𝐾 ) )
30	20 28 29	syl2an	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ 𝑀 ↔ ( 𝐾 − 𝑀 ) ≤ 𝐾 ) )
31	27 30	mpbid	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 − 𝑀 ) ≤ 𝐾 )
32	31	anim1i	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝐾 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) )
33		letr	⊢ ( ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐾 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
34	25 32 33	sylc	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
35	34	exp31	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑁 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
36	35	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑁 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
37	36	com14	⊢ ( 𝐾 ≤ 𝑁 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
38	37	adantl	⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
39	38	impcom	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
40	14 39	sylbi	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
41	40	com13	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
42	41	impcom	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
43	42	3adant3	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
44	13 43	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
45	44	imp	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
46	45	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
47	10 12 46	3jca	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
48	1 47	mpancom	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
49		elfz2nn0	⊢ ( ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
50	48 49	sylibr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )