Metamath Proof Explorer

Theorem btwnnz

Description: A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion btwnnz ⊢ A ∈ ℤ ∧ A < B ∧ B < A + 1 → ¬ B ∈ ℤ

Proof

Step Hyp Ref Expression
1 zltp1le ⊢ A ∈ ℤ ∧ B ∈ ℤ → A < B ↔ A + 1 ≤ B
2 peano2z ⊢ A ∈ ℤ → A + 1 ∈ ℤ
3 zre ⊢ A + 1 ∈ ℤ → A + 1 ∈ ℝ
4 2 3 syl ⊢ A ∈ ℤ → A + 1 ∈ ℝ
5 zre ⊢ B ∈ ℤ → B ∈ ℝ
6 lenlt ⊢ A + 1 ∈ ℝ ∧ B ∈ ℝ → A + 1 ≤ B ↔ ¬ B < A + 1
7 4 5 6 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + 1 ≤ B ↔ ¬ B < A + 1
8 1 7 bitrd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A < B ↔ ¬ B < A + 1
9 8 biimpd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A < B → ¬ B < A + 1
10 9 impancom ⊢ A ∈ ℤ ∧ A < B → B ∈ ℤ → ¬ B < A + 1
11 10 con2d ⊢ A ∈ ℤ ∧ A < B → B < A + 1 → ¬ B ∈ ℤ
12 11 3impia ⊢ A ∈ ℤ ∧ A < B ∧ B < A + 1 → ¬ B ∈ ℤ