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∈ℤ