This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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