Metamath Proof Explorer

Theorem fllt

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

Ref Expression
Assertion fllt ⊢ A ∈ ℝ ∧ B ∈ ℤ → A < B ↔ A < B

Proof

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