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 ¬ ( 𝑁 + 1 ) ∈ ( 𝑀 ... 𝑁 )

Proof

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