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	⊢ ( 𝐴 ∈ ℝ → ( ( ⌈ ‘ 𝐴 ) − 1 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
2	1	oveq1d	⊢ ( 𝐴 ∈ ℝ → ( ( ⌈ ‘ 𝐴 ) − 1 ) = ( - ( ⌊ ‘ - 𝐴 ) − 1 ) )
3		ceim1l	⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 )
4	2 3	eqbrtrd	⊢ ( 𝐴 ∈ ℝ → ( ( ⌈ ‘ 𝐴 ) − 1 ) < 𝐴 )