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	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ ( ⌈ ‘ 𝐴 ) )