uzm1

Description: Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	uzm1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
2	1	a1d	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to M \in ℤ)$
3		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
4		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
5	3 4	syl	$⊢ N \in ℤ_{\geq M} \to N - 1 \in ℤ$
6	5	a1d	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to N - 1 \in ℤ)$
7		df-ne	$⊢ N \neq M \leftrightarrow \neg N = M$
8		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
9	1	zred	$⊢ N \in ℤ_{\geq M} \to M \in ℝ$
10		eluzelre	$⊢ N \in ℤ_{\geq M} \to N \in ℝ$
11	9 10	ltlend	$⊢ N \in ℤ_{\geq M} \to (M < N \leftrightarrow (M \leq N \land N \neq M))$
12	11	biimprd	$⊢ N \in ℤ_{\geq M} \to ((M \leq N \land N \neq M) \to M < N)$
13	8 12	mpand	$⊢ N \in ℤ_{\geq M} \to (N \neq M \to M < N)$
14	7 13	biimtrrid	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to M < N)$
15		zltlem1	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow M \leq N - 1)$
16	1 3 15	syl2anc	$⊢ N \in ℤ_{\geq M} \to (M < N \leftrightarrow M \leq N - 1)$
17	14 16	sylibd	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to M \leq N - 1)$
18	2 6 17	3jcad	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to (M \in ℤ \land N - 1 \in ℤ \land M \leq N - 1))$
19		eluz2	$⊢ N - 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N - 1 \in ℤ \land M \leq N - 1)$
20	18 19	imbitrrdi	$⊢ N \in ℤ_{\geq M} \to (\neg N = M \to N - 1 \in ℤ_{\geq M})$
21	20	orrd	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$

Metamath Proof Explorer