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	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to K \in (N - M \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfz2	$⊢ K \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land K \in ℤ) \land (0 \leq K \land K \leq N))$
2		3simpc	$⊢ (0 \in ℤ \land N \in ℤ \land K \in ℤ) \to (N \in ℤ \land K \in ℤ)$
3	2	adantr	$⊢ ((0 \in ℤ \land N \in ℤ \land K \in ℤ) \land (0 \leq K \land K \leq N)) \to (N \in ℤ \land K \in ℤ)$
4	1 3	sylbi	$⊢ K \in (0 \dots N) \to (N \in ℤ \land K \in ℤ)$
5	4	anim2i	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to (M \in ℤ \land (N \in ℤ \land K \in ℤ))$
6		simpl	$⊢ (N \in ℤ \land K \in ℤ) \to N \in ℤ$
7	6	anim2i	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to (M \in ℤ \land N \in ℤ)$
8	7	ancomd	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to (N \in ℤ \land M \in ℤ)$
9		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
10	8 9	syl	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to N - M \in ℤ$
11	6	adantl	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to N \in ℤ$
12		simprr	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to K \in ℤ$
13	10 11 12	3jca	$⊢ (M \in ℤ \land (N \in ℤ \land K \in ℤ)) \to (N - M \in ℤ \land N \in ℤ \land K \in ℤ)$
14	5 13	syl	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to (N - M \in ℤ \land N \in ℤ \land K \in ℤ)$
15	14	3adant3	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to (N - M \in ℤ \land N \in ℤ \land K \in ℤ)$
16		elfzel2	$⊢ K \in (0 \dots N) \to N \in ℤ$
17	16	zred	$⊢ K \in (0 \dots N) \to N \in ℝ$
18	17	adantl	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to N \in ℝ$
19		zre	$⊢ M \in ℤ \to M \in ℝ$
20	19	adantr	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to M \in ℝ$
21		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
22	21	zred	$⊢ K \in (0 \dots N) \to K \in ℝ$
23	22	adantl	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to K \in ℝ$
24	18 20 23	3jca	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to (N \in ℝ \land M \in ℝ \land K \in ℝ)$
25		simp1	$⊢ (N \in ℝ \land M \in ℝ \land K \in ℝ) \to N \in ℝ$
26		readdcl	$⊢ (M \in ℝ \land K \in ℝ) \to M + K \in ℝ$
27	26	3adant1	$⊢ (N \in ℝ \land M \in ℝ \land K \in ℝ) \to M + K \in ℝ$
28		ltle	$⊢ (N \in ℝ \land M + K \in ℝ) \to (N < M + K \to N \leq M + K)$
29	25 27 28	syl2anc	$⊢ (N \in ℝ \land M \in ℝ \land K \in ℝ) \to (N < M + K \to N \leq M + K)$
30		lesubadd2	$⊢ (N \in ℝ \land M \in ℝ \land K \in ℝ) \to (N - M \leq K \leftrightarrow N \leq M + K)$
31	29 30	sylibrd	$⊢ (N \in ℝ \land M \in ℝ \land K \in ℝ) \to (N < M + K \to N - M \leq K)$
32	24 31	syl	$⊢ (M \in ℤ \land K \in (0 \dots N)) \to (N < M + K \to N - M \leq K)$
33	32	3impia	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to N - M \leq K$
34		elfzle2	$⊢ K \in (0 \dots N) \to K \leq N$
35	34	3ad2ant2	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to K \leq N$
36	15 33 35	jca32	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to ((N - M \in ℤ \land N \in ℤ \land K \in ℤ) \land (N - M \leq K \land K \leq N))$
37		elfz2	$⊢ K \in (N - M \dots N) \leftrightarrow ((N - M \in ℤ \land N \in ℤ \land K \in ℤ) \land (N - M \leq K \land K \leq N))$
38	36 37	sylibr	$⊢ (M \in ℤ \land K \in (0 \dots N) \land N < M + K) \to K \in (N - M \dots N)$

Metamath Proof Explorer

Theorem elfzelfzlble

Proof