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 ( 𝐵 ∈ ℤ → ( 𝐴 ∈ ( ℤ ∖ ( ℤ ‘ ( 𝐵 + 1 ) ) ) ↔ ( 𝐴 ∈ ℤ ∧ 𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eldif ( 𝐴 ∈ ( ℤ ∖ ( ℤ ‘ ( 𝐵 + 1 ) ) ) ↔ ( 𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ) )
2 zltp1le ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐵 < 𝐴 ↔ ( 𝐵 + 1 ) ≤ 𝐴 ) )
3 2 notbid ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( 𝐵 + 1 ) ≤ 𝐴 ) )
4 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
5 zre ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
6 lenlt ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
7 4 5 6 syl2anr ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
8 peano2z ( 𝐵 ∈ ℤ → ( 𝐵 + 1 ) ∈ ℤ )
9 eluz ( ( ( 𝐵 + 1 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ↔ ( 𝐵 + 1 ) ≤ 𝐴 ) )
10 8 9 sylan ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ↔ ( 𝐵 + 1 ) ≤ 𝐴 ) )
11 10 notbid ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ↔ ¬ ( 𝐵 + 1 ) ≤ 𝐴 ) )
12 3 7 11 3bitr4rd ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ↔ 𝐴𝐵 ) )
13 12 pm5.32da ( 𝐵 ∈ ℤ → ( ( 𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈ ( ℤ ‘ ( 𝐵 + 1 ) ) ) ↔ ( 𝐴 ∈ ℤ ∧ 𝐴𝐵 ) ) )
14 1 13 syl5bb ( 𝐵 ∈ ℤ → ( 𝐴 ∈ ( ℤ ∖ ( ℤ ‘ ( 𝐵 + 1 ) ) ) ↔ ( 𝐴 ∈ ℤ ∧ 𝐴𝐵 ) ) )