Metamath Proof Explorer

Theorem fzonfzoufzol

Description: If an element of a half-open integer range is not in the upper part of the range, it is in the lower part of the range. (Contributed by Alexander van der Vekens, 29-Oct-2018)

		Ref	Expression
	Assertion	fzonfzoufzol	$⊢ (M \in ℤ \land M < N \land I \in (0 ..^N)) \to (\neg I \in (N - M ..^N) \to I \in (0 ..^N - M))$

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	$⊢ I \in (0 ..^N) \to N \in ℤ$
2		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
3	2	ex	$⊢ N \in ℤ \to (M \in ℤ \to N - M \in ℤ)$
4	1 3	syl	$⊢ I \in (0 ..^N) \to (M \in ℤ \to N - M \in ℤ)$
5	4	impcom	$⊢ (M \in ℤ \land I \in (0 ..^N)) \to N - M \in ℤ$
6	5	3adant2	$⊢ (M \in ℤ \land M < N \land I \in (0 ..^N)) \to N - M \in ℤ$
7	6	adantr	$⊢ ((M \in ℤ \land M < N \land I \in (0 ..^N)) \land \neg I \in (0 ..^N - M)) \to N - M \in ℤ$
8		simp3	$⊢ (M \in ℤ \land M < N \land I \in (0 ..^N)) \to I \in (0 ..^N)$
9	8	anim1i	$⊢ ((M \in ℤ \land M < N \land I \in (0 ..^N)) \land \neg I \in (0 ..^N - M)) \to (I \in (0 ..^N) \land \neg I \in (0 ..^N - M))$
10		elfzonelfzo	$⊢ N - M \in ℤ \to ((I \in (0 ..^N) \land \neg I \in (0 ..^N - M)) \to I \in (N - M ..^N))$
11	7 9 10	sylc	$⊢ ((M \in ℤ \land M < N \land I \in (0 ..^N)) \land \neg I \in (0 ..^N - M)) \to I \in (N - M ..^N)$
12	11	ex	$⊢ (M \in ℤ \land M < N \land I \in (0 ..^N)) \to (\neg I \in (0 ..^N - M) \to I \in (N - M ..^N))$
13	12	con1d	$⊢ (M \in ℤ \land M < N \land I \in (0 ..^N)) \to (\neg I \in (N - M ..^N) \to I \in (0 ..^N - M))$