Metamath Proof Explorer

Theorem fzp1nel

Description: One plus the upper bound of a finite set of integers is not a member of that set. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Assertion fzp1nel ⊢¬N+1∈M…N

Proof

Step Hyp Ref Expression
1 zre ⊢N∈ℤ→N∈ℝ
2 ltp1 ⊢N∈ℝ→N<N+1
3 id ⊢N∈ℝ→N∈ℝ
4 peano2re ⊢N∈ℝ→N+1∈ℝ
5 3 4 ltnled ⊢N∈ℝ→N<N+1↔¬N+1≤N
6 2 5 mpbid ⊢N∈ℝ→¬N+1≤N
7 1 6 syl ⊢N∈ℤ→¬N+1≤N
8 7 intnand ⊢N∈ℤ→¬M≤N+1∧N+1≤N
9 8 3ad2ant2 ⊢M∈ℤ∧N∈ℤ∧N+1∈ℤ→¬M≤N+1∧N+1≤N
10 elfz2 ⊢N+1∈M…N↔M∈ℤ∧N∈ℤ∧N+1∈ℤ∧M≤N+1∧N+1≤N
11 10 notbii ⊢¬N+1∈M…N↔¬M∈ℤ∧N∈ℤ∧N+1∈ℤ∧M≤N+1∧N+1≤N
12 imnan ⊢M∈ℤ∧N∈ℤ∧N+1∈ℤ→¬M≤N+1∧N+1≤N↔¬M∈ℤ∧N∈ℤ∧N+1∈ℤ∧M≤N+1∧N+1≤N
13 11 12 bitr4i ⊢¬N+1∈M…N↔M∈ℤ∧N∈ℤ∧N+1∈ℤ→¬M≤N+1∧N+1≤N
14 9 13 mpbir ⊢¬N+1∈M…N