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