Theorem elfzo2

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		an4	⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
2		df-3an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) )
3	2	anbi1i	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
4		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
5		3ancoma	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
6		df-3an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) )
7	4 5 6	3bitri	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) )
8	7	anbi1i	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
9	1 3 8	3bitr4i	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
10		elfzoelz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
11		elfzoel1	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
12		elfzoel2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
13	10 11 12	3jca	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
14		elfzo	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
15	13 14	biadanii	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
16		3anass	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
17	9 15 16	3bitr4i	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )