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