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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → ( ⌈ ‘ 𝐴 ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
3		ceile	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 )
4	2 3	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → ( ⌈ ‘ 𝐴 ) ≤ 𝐵 )