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