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

Proof

Step	Hyp	Ref	Expression
1		elfz2	$⊢ K \in (M \dots M + N) \leftrightarrow ((M \in ℤ \land M + N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq M + N))$
2		znn0sub	$⊢ (M \in ℤ \land K \in ℤ) \to (M \leq K \leftrightarrow K - M \in ℕ_{0})$
3	2	adantr	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (M \leq K \leftrightarrow K - M \in ℕ_{0})$
4	3	biimpcd	$⊢ M \leq K \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to K - M \in ℕ_{0})$
5	4	adantr	$⊢ (M \leq K \land K \leq M + N) \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to K - M \in ℕ_{0})$
6	5	impcom	$⊢ (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \land (M \leq K \land K \leq M + N)) \to K - M \in ℕ_{0}$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8	7	adantr	$⊢ (M \in ℤ \land K \in ℤ) \to M \in ℝ$
9	8	adantr	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to M \in ℝ$
10		zre	$⊢ K \in ℤ \to K \in ℝ$
11	10	adantl	$⊢ (M \in ℤ \land K \in ℤ) \to K \in ℝ$
12	11	adantr	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to K \in ℝ$
13		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
14	13	adantlr	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to M + N \in ℤ$
15	14	zred	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to M + N \in ℝ$
16		letr	$⊢ (M \in ℝ \land K \in ℝ \land M + N \in ℝ) \to ((M \leq K \land K \leq M + N) \to M \leq M + N)$
17	9 12 15 16	syl3anc	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to ((M \leq K \land K \leq M + N) \to M \leq M + N)$
18		zre	$⊢ N \in ℤ \to N \in ℝ$
19		addge01	$⊢ (M \in ℝ \land N \in ℝ) \to (0 \leq N \leftrightarrow M \leq M + N)$
20	8 18 19	syl2an	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (0 \leq N \leftrightarrow M \leq M + N)$
21		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
22	21	simplbi2	$⊢ N \in ℤ \to (0 \leq N \to N \in ℕ_{0})$
23	22	adantl	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (0 \leq N \to N \in ℕ_{0})$
24	20 23	sylbird	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (M \leq M + N \to N \in ℕ_{0})$
25	17 24	syld	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to ((M \leq K \land K \leq M + N) \to N \in ℕ_{0})$
26	25	imp	$⊢ (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \land (M \leq K \land K \leq M + N)) \to N \in ℕ_{0}$
27		df-3an	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ) \leftrightarrow ((M \in ℤ \land K \in ℤ) \land N \in ℤ)$
28		3ancoma	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ) \leftrightarrow (K \in ℤ \land M \in ℤ \land N \in ℤ)$
29	27 28	bitr3i	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \leftrightarrow (K \in ℤ \land M \in ℤ \land N \in ℤ)$
30	10 7 18	3anim123i	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℝ \land M \in ℝ \land N \in ℝ)$
31	29 30	sylbi	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (K \in ℝ \land M \in ℝ \land N \in ℝ)$
32		lesubadd2	$⊢ (K \in ℝ \land M \in ℝ \land N \in ℝ) \to (K - M \leq N \leftrightarrow K \leq M + N)$
33	31 32	syl	$⊢ ((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (K - M \leq N \leftrightarrow K \leq M + N)$
34	33	biimprcd	$⊢ K \leq M + N \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to K - M \leq N)$
35	34	adantl	$⊢ (M \leq K \land K \leq M + N) \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to K - M \leq N)$
36	35	impcom	$⊢ (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \land (M \leq K \land K \leq M + N)) \to K - M \leq N$
37	6 26 36	3jca	$⊢ (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \land (M \leq K \land K \leq M + N)) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
38	37	exp31	$⊢ (M \in ℤ \land K \in ℤ) \to (N \in ℤ \to ((M \leq K \land K \leq M + N) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)))$
39	38	com23	$⊢ (M \in ℤ \land K \in ℤ) \to ((M \leq K \land K \leq M + N) \to (N \in ℤ \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)))$
40	39	3adant2	$⊢ (M \in ℤ \land M + N \in ℤ \land K \in ℤ) \to ((M \leq K \land K \leq M + N) \to (N \in ℤ \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)))$
41	40	imp	$⊢ ((M \in ℤ \land M + N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq M + N)) \to (N \in ℤ \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N))$
42	41	com12	$⊢ N \in ℤ \to (((M \in ℤ \land M + N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq M + N)) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N))$
43	1 42	syl5bi	$⊢ N \in ℤ \to (K \in (M \dots M + N) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N))$
44	43	imp	$⊢ (N \in ℤ \land K \in (M \dots M + N)) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
45		elfz2nn0	$⊢ K - M \in (0 \dots N) \leftrightarrow (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
46	44 45	sylibr	$⊢ (N \in ℤ \land K \in (M \dots M + N)) \to K - M \in (0 \dots N)$

Metamath Proof Explorer

Theorem elfzmlbp

Proof