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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 𝐵 ∧ 𝐵 < ( 𝐴 + 1 ) ) → ¬ 𝐵 ∈ ℤ )

Proof

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