Theorem elfzo1

Description: Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017)

	Ref	Expression
Assertion	elfzo1	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		fzossnn	⊢ ( 1 ..^ 𝑀 ) ⊆ ℕ
2	1	sseli	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → 𝑁 ∈ ℕ )
3		elfzouz2	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
4		eluznn	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ )
5	2 3 4	syl2anc	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ℕ )
6		elfzolt2	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → 𝑁 < 𝑀 )
7	2 5 6	3jca	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) )
8		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
9	8	eqimssi	⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
10	9	sseli	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
11		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
12		id	⊢ ( 𝑁 < 𝑀 → 𝑁 < 𝑀 )
13	10 11 12	3anim123i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 < 𝑀 ) )
14		elfzo2	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 < 𝑀 ) )
15	13 14	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) → 𝑁 ∈ ( 1 ..^ 𝑀 ) )
16	7 15	impbii	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) )