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

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