Theorem ceilm1lt

Description: One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceilm1lt	$$⊢A\in ℝ\to ⌈A⌉-1<A$$

Proof

Step	Hyp	Ref	Expression
1		ceilval	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$
2	1	oveq1d	$$⊢A\in ℝ\to ⌈A⌉-1=-⌊-A⌋-1$$
3		ceim1l	$$⊢A\in ℝ\to -⌊-A⌋-1<A$$
4	2 3	eqbrtrd	$$⊢A\in ℝ\to ⌈A⌉-1<A$$