elfzomelpfzo

Description: An integer increased by another integer is an element of a half-open integer range if and only if the integer is contained in the half-open integer range with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018)

		Ref	Expression
	Assertion	elfzomelpfzo	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K \in (M - L ..^N - L) \leftrightarrow K + L \in (M ..^N))$

Proof

Step	Hyp	Ref	Expression
1		zsubcl	$⊢ (M \in ℤ \land L \in ℤ) \to M - L \in ℤ$
2	1	ad2ant2rl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to M - L \in ℤ$
3		simpl	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℤ$
4	3	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to M \in ℤ$
5	2 4	2thd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (M - L \in ℤ \leftrightarrow M \in ℤ)$
6		simpl	$⊢ (K \in ℤ \land L \in ℤ) \to K \in ℤ$
7	6	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to K \in ℤ$
8		zaddcl	$⊢ (K \in ℤ \land L \in ℤ) \to K + L \in ℤ$
9	8	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to K + L \in ℤ$
10	7 9	2thd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K \in ℤ \leftrightarrow K + L \in ℤ)$
11		zre	$⊢ M \in ℤ \to M \in ℝ$
12	11	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℝ$
13	12	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to M \in ℝ$
14		zre	$⊢ L \in ℤ \to L \in ℝ$
15	14	adantl	$⊢ (K \in ℤ \land L \in ℤ) \to L \in ℝ$
16	15	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to L \in ℝ$
17		zre	$⊢ K \in ℤ \to K \in ℝ$
18	17	adantr	$⊢ (K \in ℤ \land L \in ℤ) \to K \in ℝ$
19	18	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to K \in ℝ$
20	13 16 19	lesubaddd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (M - L \leq K \leftrightarrow M \leq K + L)$
21	5 10 20	3anbi123d	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to ((M - L \in ℤ \land K \in ℤ \land M - L \leq K) \leftrightarrow (M \in ℤ \land K + L \in ℤ \land M \leq K + L))$
22		eluz2	$⊢ K \in ℤ_{\geq (M - L)} \leftrightarrow (M - L \in ℤ \land K \in ℤ \land M - L \leq K)$
23		eluz2	$⊢ K + L \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land K + L \in ℤ \land M \leq K + L)$
24	21 22 23	3bitr4g	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K \in ℤ_{\geq (M - L)} \leftrightarrow K + L \in ℤ_{\geq M})$
25		zsubcl	$⊢ (N \in ℤ \land L \in ℤ) \to N - L \in ℤ$
26	25	ad2ant2l	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to N - L \in ℤ$
27		simplr	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to N \in ℤ$
28	26 27	2thd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (N - L \in ℤ \leftrightarrow N \in ℤ)$
29		zre	$⊢ N \in ℤ \to N \in ℝ$
30	29	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℝ$
31	30	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to N \in ℝ$
32	19 16 31	ltaddsubd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K + L < N \leftrightarrow K < N - L)$
33	32	bicomd	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K < N - L \leftrightarrow K + L < N)$
34	24 28 33	3anbi123d	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to ((K \in ℤ_{\geq (M - L)} \land N - L \in ℤ \land K < N - L) \leftrightarrow (K + L \in ℤ_{\geq M} \land N \in ℤ \land K + L < N))$
35		elfzo2	$⊢ K \in (M - L ..^N - L) \leftrightarrow (K \in ℤ_{\geq (M - L)} \land N - L \in ℤ \land K < N - L)$
36		elfzo2	$⊢ K + L \in (M ..^N) \leftrightarrow (K + L \in ℤ_{\geq M} \land N \in ℤ \land K + L < N)$
37	34 35 36	3bitr4g	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to (K \in (M - L ..^N - L) \leftrightarrow K + L \in (M ..^N))$

Metamath Proof Explorer

Theorem elfzomelpfzo

Proof