Metamath Proof Explorer

Theorem ellz1

Description: Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion ellz1 ⊢ B ∈ ℤ → A ∈ ℤ ∖ ℤ ≥ B + 1 ↔ A ∈ ℤ ∧ A ≤ B

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ ℤ ∖ ℤ ≥ B + 1 ↔ A ∈ ℤ ∧ ¬ A ∈ ℤ ≥ B + 1
2 zltp1le ⊢ B ∈ ℤ ∧ A ∈ ℤ → B < A ↔ B + 1 ≤ A
3 2 notbid ⊢ B ∈ ℤ ∧ A ∈ ℤ → ¬ B < A ↔ ¬ B + 1 ≤ A
4 zre ⊢ A ∈ ℤ → A ∈ ℝ
5 zre ⊢ B ∈ ℤ → B ∈ ℝ
6 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
7 4 5 6 syl2anr ⊢ B ∈ ℤ ∧ A ∈ ℤ → A ≤ B ↔ ¬ B < A
8 peano2z ⊢ B ∈ ℤ → B + 1 ∈ ℤ
9 eluz ⊢ B + 1 ∈ ℤ ∧ A ∈ ℤ → A ∈ ℤ ≥ B + 1 ↔ B + 1 ≤ A
10 8 9 sylan ⊢ B ∈ ℤ ∧ A ∈ ℤ → A ∈ ℤ ≥ B + 1 ↔ B + 1 ≤ A
11 10 notbid ⊢ B ∈ ℤ ∧ A ∈ ℤ → ¬ A ∈ ℤ ≥ B + 1 ↔ ¬ B + 1 ≤ A
12 3 7 11 3bitr4rd ⊢ B ∈ ℤ ∧ A ∈ ℤ → ¬ A ∈ ℤ ≥ B + 1 ↔ A ≤ B
13 12 pm5.32da ⊢ B ∈ ℤ → A ∈ ℤ ∧ ¬ A ∈ ℤ ≥ B + 1 ↔ A ∈ ℤ ∧ A ≤ B
14 1 13 bitrid ⊢ B ∈ ℤ → A ∈ ℤ ∖ ℤ ≥ B + 1 ↔ A ∈ ℤ ∧ A ≤ B