Theorem ceilge

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

	Ref	Expression
Assertion	ceilge	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ⌈ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ceige	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ - ( ⌊ ‘ - 𝐴 ) )
2		ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
3	1 2	breqtrrd	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ⌈ ‘ 𝐴 ) )