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 ( 𝜑𝐴 ∈ ℝ )
Assertion ceilged ( 𝜑𝐴 ≤ ( ⌈ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ceilged.1 ( 𝜑𝐴 ∈ ℝ )
2 ceilge ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ⌈ ‘ 𝐴 ) )
3 1 2 syl ( 𝜑𝐴 ≤ ( ⌈ ‘ 𝐴 ) )