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