Theorem elfzmlbp

Description: Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018)

	Ref	Expression
Assertion	elfzmlbp	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2	⊢ ( 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) )
2		znn0sub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
3	2	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
4	3	biimpcd	⊢ ( 𝑀 ≤ 𝐾 → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
5	4	adantr	⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
6	5	impcom	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
7		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8	7	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑀 ∈ ℝ )
9	8	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
10		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
11	10	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ )
12	11	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℝ )
13		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
14	13	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
15	14	zred	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
16		letr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
17	9 12 15 16	syl3anc	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
18		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
19		addge01	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
20	8 18 19	syl2an	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
21		elnn0z	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
22	21	simplbi2	⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
23	22	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
24	20 23	sylbird	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ ( 𝑀 + 𝑁 ) → 𝑁 ∈ ℕ0 ) )
25	17 24	syld	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑁 ∈ ℕ0 ) )
26	25	imp	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
27		df-3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) )
28		3ancoma	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
29	27 28	bitr3i	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
30	10 7 18	3anim123i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
31	29 30	sylbi	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
32		lesubadd2	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐾 − 𝑀 ) ≤ 𝑁 ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
33	31 32	syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 − 𝑀 ) ≤ 𝑁 ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
34	33	biimprcd	⊢ ( 𝐾 ≤ ( 𝑀 + 𝑁 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
35	34	adantl	⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
36	35	impcom	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
37	6 26 36	3jca	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
38	37	exp31	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
39	38	com23	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
40	39	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
41	40	imp	⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
42	41	com12	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
43	1 42	biimtrid	⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
44	43	imp	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
45		elfz2nn0	⊢ ( ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
46	44 45	sylibr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )