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

Proof

Step Hyp Ref Expression
1 ltflcei ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ 𝐵 ) < 𝐴 ↔ 𝐵 < - ( ⌊ ‘ - 𝐴 ) ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ⌊ ‘ 𝐵 ) < 𝐴 ↔ 𝐵 < - ( ⌊ ‘ - 𝐴 ) ) )
3 2 notbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ ( ⌊ ‘ 𝐵 ) < 𝐴 ↔ ¬ 𝐵 < - ( ⌊ ‘ - 𝐴 ) ) )
4 reflcl ⊢ ( 𝐵 ∈ ℝ → ( ⌊ ‘ 𝐵 ) ∈ ℝ )
5 lenlt ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐵 ) ∈ ℝ ) → ( 𝐴 ≤ ( ⌊ ‘ 𝐵 ) ↔ ¬ ( ⌊ ‘ 𝐵 ) < 𝐴 ) )
6 4 5 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ ( ⌊ ‘ 𝐵 ) ↔ ¬ ( ⌊ ‘ 𝐵 ) < 𝐴 ) )
7 ceicl ⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℤ )
8 7 zred ⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
9 lenlt ⊢ ( ( - ( ⌊ ‘ - 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ↔ ¬ 𝐵 < - ( ⌊ ‘ - 𝐴 ) ) )
10 8 9 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ↔ ¬ 𝐵 < - ( ⌊ ‘ - 𝐴 ) ) )
11 3 6 10 3bitr4rd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - ( ⌊ ‘ - 𝐴 ) ≤ 𝐵 ↔ 𝐴 ≤ ( ⌊ ‘ 𝐵 ) ) )