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

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

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 ℤ$
4	3	zred	$⊢ A \in ℝ \to ⌈A⌉ \in ℝ$
5		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
6		ceilge	$⊢ A \in ℝ \to A \leq ⌈A⌉$
7	1 2 4 5 6	letrd	$⊢ A \in ℝ \to ⌊A⌋ \leq ⌈A⌉$