Theorem uzm1

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

	Ref	Expression
Assertion	uzm1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
2	1	a1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → 𝑀 ∈ ℤ ) )
3		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
4		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
5	3 4	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
6	5	a1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → ( 𝑁 − 1 ) ∈ ℤ ) )
7		df-ne	⊢ ( 𝑁 ≠ 𝑀 ↔ ¬ 𝑁 = 𝑀 )
8		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
9	1	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
10		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )
11	9 10	ltlend	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀 ) ) )
12	11	biimprd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀 ) → 𝑀 < 𝑁 ) )
13	8 12	mpand	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ≠ 𝑀 → 𝑀 < 𝑁 ) )
14	7 13	syl5bir	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → 𝑀 < 𝑁 ) )
15		zltlem1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 1 ) ) )
16	1 3 15	syl2anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 < 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 1 ) ) )
17	14 16	sylibd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → 𝑀 ≤ ( 𝑁 − 1 ) ) )
18	2 6 17	3jcad	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 1 ) ) ) )
19		eluz2	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 1 ) ) )
20	18 19	syl6ibr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
21	20	orrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )