Metamath Proof Explorer


Theorem elfz1b

Description: Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018) (Proof shortened by AV, 23-Jan-2022)

Ref Expression
Assertion elfz1b ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁𝑀 ) )

Proof

Step Hyp Ref Expression
1 elfz2 ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁𝑁𝑀 ) ) )
2 simpl2 ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁𝑁𝑀 ) ) → 𝑀 ∈ ℤ )
3 1red ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℝ )
4 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
5 4 3ad2ant3 ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
6 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
7 6 3ad2ant2 ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
8 letr ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 1 ≤ 𝑁𝑁𝑀 ) → 1 ≤ 𝑀 ) )
9 3 5 7 8 syl3anc ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 1 ≤ 𝑁𝑁𝑀 ) → 1 ≤ 𝑀 ) )
10 9 imp ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁𝑁𝑀 ) ) → 1 ≤ 𝑀 )
11 elnnz1 ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ) )
12 2 10 11 sylanbrc ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁𝑁𝑀 ) ) → 𝑀 ∈ ℕ )
13 1 12 sylbi ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℕ )
14 elfzel2 ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℤ )
15 fznn ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
16 15 biimpd ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
17 14 16 mpcom ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) )
18 3anan12 ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
19 13 17 18 sylanbrc ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁𝑀 ) )
20 nnz ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
21 20 15 syl ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
22 21 biimprd ( 𝑀 ∈ ℕ → ( ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) → 𝑁 ∈ ( 1 ... 𝑀 ) ) )
23 22 expd ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝑁𝑀𝑁 ∈ ( 1 ... 𝑀 ) ) ) )
24 23 3imp21 ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁𝑀 ) → 𝑁 ∈ ( 1 ... 𝑀 ) )
25 19 24 impbii ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁𝑀 ) )