Theorem ceige

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007)

	Ref	Expression
Assertion	ceige	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ - ( ⌊ ‘ - 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
2		reflcl	⊢ ( - 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
4		flle	⊢ ( - 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ≤ - 𝐴 )
5	1 4	syl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ≤ - 𝐴 )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ - 𝐴 ) ∈ ℝ ) → ( ⌊ ‘ - 𝐴 ) ≤ - 𝐴 )
7		lenegcon2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ - 𝐴 ) ∈ ℝ ) → ( 𝐴 ≤ - ( ⌊ ‘ - 𝐴 ) ↔ ( ⌊ ‘ - 𝐴 ) ≤ - 𝐴 ) )
8	6 7	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ - 𝐴 ) ∈ ℝ ) → 𝐴 ≤ - ( ⌊ ‘ - 𝐴 ) )
9	3 8	mpdan	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ - ( ⌊ ‘ - 𝐴 ) )