Metamath Proof Explorer


Theorem ceilged

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis ceilged.1
|- ( ph -> A e. RR )
Assertion ceilged
|- ( ph -> A <_ ( |^ ` A ) )

Proof

Step Hyp Ref Expression
1 ceilged.1
 |-  ( ph -> A e. RR )
2 ceilge
 |-  ( A e. RR -> A <_ ( |^ ` A ) )
3 1 2 syl
 |-  ( ph -> A <_ ( |^ ` A ) )