Metamath Proof Explorer

Theorem leceifl

Description: Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017)

Ref Expression
Assertion leceifl ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − A ≤ B ↔ A ≤ B

Proof

Step Hyp Ref Expression
1 ltflcei ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ B < − − A
2 1 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B < − − A
3 2 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B < A ↔ ¬ B < − − A
4 reflcl ⊢ B ∈ ℝ → B ∈ ℝ
5 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
6 4 5 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
7 ceicl ⊢ A ∈ ℝ → − − A ∈ ℤ
8 7 zred ⊢ A ∈ ℝ → − − A ∈ ℝ
9 lenlt ⊢ − − A ∈ ℝ ∧ B ∈ ℝ → − − A ≤ B ↔ ¬ B < − − A
10 8 9 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − A ≤ B ↔ ¬ B < − − A
11 3 6 10 3bitr4rd ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − A ≤ B ↔ A ≤ B