This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → 𝑀 < 𝑁 ) )
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 imbitrrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑁 = 𝑀 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
21 20 orrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )