Theorem elfzelfzlble

Description: Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		elfz2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
2		3simpc	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
3	2	adantr	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
4	1 3	sylbi	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
5	4	anim2i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) )
6		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
7	6	anim2i	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
8	7	ancomd	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
9		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
10	8 9	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
11	6	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
12		simprr	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
13	10 11 12	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
14	5 13	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
15	14	3adant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 < ( 𝑀 + 𝐾 ) ) → ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
16		elfzel2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
17	16	zred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
18	17	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
19		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
20	19	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
21		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
22	21	zred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℝ )
23	22	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
24	18 20 23	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
25		simp1	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → 𝑁 ∈ ℝ )
26		readdcl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 + 𝐾 ) ∈ ℝ )
27	26	3adant1	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 + 𝐾 ) ∈ ℝ )
28		ltle	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑀 + 𝐾 ) ∈ ℝ ) → ( 𝑁 < ( 𝑀 + 𝐾 ) → 𝑁 ≤ ( 𝑀 + 𝐾 ) ) )
29	25 27 28	syl2anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑁 < ( 𝑀 + 𝐾 ) → 𝑁 ≤ ( 𝑀 + 𝐾 ) ) )
30		lesubadd2	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑁 − 𝑀 ) ≤ 𝐾 ↔ 𝑁 ≤ ( 𝑀 + 𝐾 ) ) )
31	29 30	sylibrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑁 < ( 𝑀 + 𝐾 ) → ( 𝑁 − 𝑀 ) ≤ 𝐾 ) )
32	24 31	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < ( 𝑀 + 𝐾 ) → ( 𝑁 − 𝑀 ) ≤ 𝐾 ) )
33	32	3impia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 < ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝑀 ) ≤ 𝐾 )
34		elfzle2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
35	34	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 < ( 𝑀 + 𝐾 ) ) → 𝐾 ≤ 𝑁 )
36	15 33 35	jca32	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 < ( 𝑀 + 𝐾 ) ) → ( ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑁 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
37		elfz2	⊢ ( 𝐾 ∈ ( ( 𝑁 − 𝑀 ) ... 𝑁 ) ↔ ( ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑁 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
38	36 37	sylibr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 < ( 𝑀 + 𝐾 ) ) → 𝐾 ∈ ( ( 𝑁 − 𝑀 ) ... 𝑁 ) )