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