Theorem elfzo3

Description: Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. K e. ( ZZ>=M ) <-> M <_ K , K e. ( K ..^ N ) <-> K < N . (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	elfzo3	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anass	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
2		elfzo2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
3		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
4		fzolb	⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
5		3anass	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
6	4 5	bitri	⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
7	6	baib	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
8	3 7	syl	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
9	8	pm5.32i	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
10	1 2 9	3bitr4i	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) )