This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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