Metamath Proof Explorer


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 A 1 < A

Proof

Step Hyp Ref Expression
1 ceilval A A = A
2 1 oveq1d A A 1 = - A - 1
3 ceim1l A - A - 1 < A
4 2 3 eqbrtrd A A 1 < A