Metamath Proof Explorer

Theorem ceille

Description: The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018)

Ref Expression
Assertion ceille ⊢ A ∈ ℝ ∧ B ∈ ℤ ∧ A ≤ B → A ≤ B

Proof

Step Hyp Ref Expression
1 ceilval ⊢ A ∈ ℝ → A = − − A
2 1 3ad2ant1 ⊢ A ∈ ℝ ∧ B ∈ ℤ ∧ A ≤ B → A = − − A
3 ceile ⊢ A ∈ ℝ ∧ B ∈ ℤ ∧ A ≤ B → − − A ≤ B
4 2 3 eqbrtrd ⊢ A ∈ ℝ ∧ B ∈ ℤ ∧ A ≤ B → A ≤ B