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

Metamath Proof Explorer

Theorem ceilge

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

		Ref	Expression
	Assertion	ceilge	$⊢ A \in ℝ \to A \leq ⌈A⌉$

Step	Hyp	Ref	Expression
1		ceige	$⊢ A \in ℝ \to A \leq - ⌊- A⌋$
2		ceilval	$⊢ A \in ℝ \to ⌈A⌉ = - ⌊- A⌋$
3	1 2	breqtrrd	$⊢ A \in ℝ \to A \leq ⌈A⌉$