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 ⊢ N ∈ 1 … M ↔ N ∈ ℕ ∧ M ∈ ℕ ∧ N ≤ M

Proof

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