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

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