Theorem ceile

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

	Ref	Expression
Assertion	ceile	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ceim1l	⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 )
3		ceicl	⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℤ )
4		zre	⊢ ( - ( ⌊ ‘ - 𝐴 ) ∈ ℤ → - ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
5		peano2rem	⊢ ( - ( ⌊ ‘ - 𝐴 ) ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) ∈ ℝ )
6	3 4 5	3syl	⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) ∈ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) ∈ ℝ )
8		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℝ )
9		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℝ )
11		ltletr	⊢ ( ( ( - ( ⌊ ‘ - 𝐴 ) − 1 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝐵 ) → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐵 ) )
12	7 8 10 11	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝐵 ) → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐵 ) )
13	2 12	mpand	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ≤ 𝐵 → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐵 ) )
14		zlem1lt	⊢ ( ( - ( ⌊ ‘ - 𝐴 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ↔ ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐵 ) )
15	3 14	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ↔ ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐵 ) )
16	13 15	sylibrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ≤ 𝐵 → - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ) )
17	16	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵 ) → - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 )