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

Metamath Proof Explorer

Theorem flltp1

Description: A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion flltp1 ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 fllelt ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
2 1 simprd ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )