Theorem ceim1l

Description: One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007)

	Ref	Expression
Assertion	ceim1l	$$⊢A\in ℝ\to -⌊-A⌋-1<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	3	recnd	$$⊢A\in ℝ\to ⌊-A⌋\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6		negdi	$$⊢\left(⌊-A⌋\in ℂ\wedge 1\in ℂ\right)\to -\left(⌊-A⌋+1\right)=-⌊-A⌋+-1$$
7	4 5 6	sylancl	$$⊢A\in ℝ\to -\left(⌊-A⌋+1\right)=-⌊-A⌋+-1$$
8	4	negcld	$$⊢A\in ℝ\to -⌊-A⌋\in ℂ$$
9		negsub	$$⊢\left(-⌊-A⌋\in ℂ\wedge 1\in ℂ\right)\to -⌊-A⌋+-1=-⌊-A⌋-1$$
10	8 5 9	sylancl	$$⊢A\in ℝ\to -⌊-A⌋+-1=-⌊-A⌋-1$$
11	7 10	eqtr2d	$$⊢A\in ℝ\to -⌊-A⌋-1=-\left(⌊-A⌋+1\right)$$
12		peano2re	$$⊢⌊-A⌋\in ℝ\to ⌊-A⌋+1\in ℝ$$
13	3 12	syl	$$⊢A\in ℝ\to ⌊-A⌋+1\in ℝ$$
14		flltp1	$$⊢-A\in ℝ\to -A<⌊-A⌋+1$$
15	1 14	syl	$$⊢A\in ℝ\to -A<⌊-A⌋+1$$
16	15	adantr	$$⊢\left(A\in ℝ\wedge ⌊-A⌋+1\in ℝ\right)\to -A<⌊-A⌋+1$$
17		ltnegcon1	$$⊢\left(A\in ℝ\wedge ⌊-A⌋+1\in ℝ\right)\to \left(-A<⌊-A⌋+1\leftrightarrow -\left(⌊-A⌋+1\right)<A\right)$$
18	16 17	mpbid	$$⊢\left(A\in ℝ\wedge ⌊-A⌋+1\in ℝ\right)\to -\left(⌊-A⌋+1\right)<A$$
19	13 18	mpdan	$$⊢A\in ℝ\to -\left(⌊-A⌋+1\right)<A$$
20	11 19	eqbrtrd	$$⊢A\in ℝ\to -⌊-A⌋-1<A$$