Metamath Proof Explorer


Theorem flleceil

Description: The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018)

Ref Expression
Assertion flleceil ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ ( ⌈ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
2 id ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3 ceilcl ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℤ )
4 3 zred ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℝ )
5 flle ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
6 ceilge ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ⌈ ‘ 𝐴 ) )
7 1 2 4 5 6 letrd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ ( ⌈ ‘ 𝐴 ) )