Theorem 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 {\mathbb{Z}}_{\ge M}\to \left(N=M\vee N-1\in {\mathbb{Z}}_{\ge M}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
2	1	a1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to M\in \mathbb{Z}\right)$$
3		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
4		peano2zm	$$⊢N\in \mathbb{Z}\to N-1\in \mathbb{Z}$$
5	3 4	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N-1\in \mathbb{Z}$$
6	5	a1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to N-1\in \mathbb{Z}\right)$$
7		df-ne	$$⊢N\ne M\leftrightarrow \neg N=M$$
8		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\le N$$
9	1	zred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in ℝ$$
10		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in ℝ$$
11	9 10	ltlend	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M<N\leftrightarrow \left(M\le N\wedge N\ne M\right)\right)$$
12	11	biimprd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(M\le N\wedge N\ne M\right)\to M<N\right)$$
13	8 12	mpand	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N\ne M\to M<N\right)$$
14	7 13	syl5bir	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to M<N\right)$$
15		zltlem1	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M<N\leftrightarrow M\le N-1\right)$$
16	1 3 15	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M<N\leftrightarrow M\le N-1\right)$$
17	14 16	sylibd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to M\le N-1\right)$$
18	2 6 17	3jcad	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to \left(M\in \mathbb{Z}\wedge N-1\in \mathbb{Z}\wedge M\le N-1\right)\right)$$
19		eluz2	$$⊢N-1\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(M\in \mathbb{Z}\wedge N-1\in \mathbb{Z}\wedge M\le N-1\right)$$
20	18 19	syl6ibr	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\neg N=M\to N-1\in {\mathbb{Z}}_{\ge M}\right)$$
21	20	orrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N=M\vee N-1\in {\mathbb{Z}}_{\ge M}\right)$$