Theorem fllt

Description: The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005)

	Ref	Expression
Assertion	fllt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ) )
2		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
3		lenlt	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
4	2 3	sylan	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
6		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
7		lenlt	⊢ ( ( 𝐵 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ↔ ¬ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )
8	2 6 7	syl2anr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ↔ ¬ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )
9	1 5 8	3bitr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ¬ 𝐴 < 𝐵 ↔ ¬ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )
10	9	con4bid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )