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	$$⊢A\in ℝ\to ⌊A⌋\le ⌈A⌉$$

Proof

Step	Hyp	Ref	Expression
1		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
2		id	$$⊢A\in ℝ\to A\in ℝ$$
3		ceilcl	$$⊢A\in ℝ\to ⌈A⌉\in \mathbb{Z}$$
4	3	zred	$$⊢A\in ℝ\to ⌈A⌉\in ℝ$$
5		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
6		ceilge	$$⊢A\in ℝ\to A\le ⌈A⌉$$
7	1 2 4 5 6	letrd	$$⊢A\in ℝ\to ⌊A⌋\le ⌈A⌉$$