Metamath Proof Explorer

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 ⊢A∈ℝ∧B∈ℤ∧A≤B→−−A≤B

Proof

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