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