Theorem ceige

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007)

	Ref	Expression
Assertion	ceige	$$⊢A\in ℝ\to A\le -⌊-A⌋$$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
2		reflcl	$$⊢-A\in ℝ\to ⌊-A⌋\in ℝ$$
3	1 2	syl	$$⊢A\in ℝ\to ⌊-A⌋\in ℝ$$
4		flle	$$⊢-A\in ℝ\to ⌊-A⌋\le -A$$
5	1 4	syl	$$⊢A\in ℝ\to ⌊-A⌋\le -A$$
6	5	adantr	$$⊢\left(A\in ℝ\wedge ⌊-A⌋\in ℝ\right)\to ⌊-A⌋\le -A$$
7		lenegcon2	$$⊢\left(A\in ℝ\wedge ⌊-A⌋\in ℝ\right)\to \left(A\le -⌊-A⌋\leftrightarrow ⌊-A⌋\le -A\right)$$
8	6 7	mpbird	$$⊢\left(A\in ℝ\wedge ⌊-A⌋\in ℝ\right)\to A\le -⌊-A⌋$$
9	3 8	mpdan	$$⊢A\in ℝ\to A\le -⌊-A⌋$$