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

Metamath Proof Explorer

Theorem uzp1

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

Ref Expression
Assertion uzp1 ⊢ N ∈ ℤ ≥ M → N = M ∨ N ∈ ℤ ≥ M + 1

Proof

Step Hyp Ref Expression
1 uzm1 ⊢ N ∈ ℤ ≥ M → N = M ∨ N − 1 ∈ ℤ ≥ M
2 eluzp1p1 ⊢ N − 1 ∈ ℤ ≥ M → N - 1 + 1 ∈ ℤ ≥ M + 1
3 eluzelcn ⊢ N ∈ ℤ ≥ M → N ∈ ℂ
4 ax-1cn ⊢ 1 ∈ ℂ
5 npcan ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N - 1 + 1 = N
6 3 4 5 sylancl ⊢ N ∈ ℤ ≥ M → N - 1 + 1 = N
7 6 eleq1d ⊢ N ∈ ℤ ≥ M → N - 1 + 1 ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ≥ M + 1
8 2 7 imbitrid ⊢ N ∈ ℤ ≥ M → N − 1 ∈ ℤ ≥ M → N ∈ ℤ ≥ M + 1
9 8 orim2d ⊢ N ∈ ℤ ≥ M → N = M ∨ N − 1 ∈ ℤ ≥ M → N = M ∨ N ∈ ℤ ≥ M + 1
10 1 9 mpd ⊢ N ∈ ℤ ≥ M → N = M ∨ N ∈ ℤ ≥ M + 1