Description: Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | elfz1uz | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑀 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℕ ) | |
2 | eluzle | ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑀 ) | |
3 | 2 | adantl | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑀 ) |
4 | eluzelz | ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑀 ∈ ℤ ) | |
5 | 4 | adantl | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ ) |
6 | fznn | ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) | |
7 | 5 6 | syl | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) |
8 | 1 3 7 | mpbir2and | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑀 ) ) |