This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )

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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( ⌊ ‘ 𝐴 ) < 𝐵 ) )