This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ..^ 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀 ) )