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 \in (1 \dots M) \leftrightarrow (N \in ℕ \land M \in ℕ \land N \leq M)$

Proof

Step	Hyp	Ref	Expression
1		elfz2	$⊢ N \in (1 \dots M) \leftrightarrow ((1 \in ℤ \land M \in ℤ \land N \in ℤ) \land (1 \leq N \land N \leq M))$
2		simpl2	$⊢ ((1 \in ℤ \land M \in ℤ \land N \in ℤ) \land (1 \leq N \land N \leq M)) \to M \in ℤ$
3		1red	$⊢ (1 \in ℤ \land M \in ℤ \land N \in ℤ) \to 1 \in ℝ$
4		zre	$⊢ N \in ℤ \to N \in ℝ$
5	4	3ad2ant3	$⊢ (1 \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℝ$
6		zre	$⊢ M \in ℤ \to M \in ℝ$
7	6	3ad2ant2	$⊢ (1 \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℝ$
8		letr	$⊢ (1 \in ℝ \land N \in ℝ \land M \in ℝ) \to ((1 \leq N \land N \leq M) \to 1 \leq M)$
9	3 5 7 8	syl3anc	$⊢ (1 \in ℤ \land M \in ℤ \land N \in ℤ) \to ((1 \leq N \land N \leq M) \to 1 \leq M)$
10	9	imp	$⊢ ((1 \in ℤ \land M \in ℤ \land N \in ℤ) \land (1 \leq N \land N \leq M)) \to 1 \leq M$
11		elnnz1	$⊢ M \in ℕ \leftrightarrow (M \in ℤ \land 1 \leq M)$
12	2 10 11	sylanbrc	$⊢ ((1 \in ℤ \land M \in ℤ \land N \in ℤ) \land (1 \leq N \land N \leq M)) \to M \in ℕ$
13	1 12	sylbi	$⊢ N \in (1 \dots M) \to M \in ℕ$
14		elfzel2	$⊢ N \in (1 \dots M) \to M \in ℤ$
15		fznn	$⊢ M \in ℤ \to (N \in (1 \dots M) \leftrightarrow (N \in ℕ \land N \leq M))$
16	15	biimpd	$⊢ M \in ℤ \to (N \in (1 \dots M) \to (N \in ℕ \land N \leq M))$
17	14 16	mpcom	$⊢ N \in (1 \dots M) \to (N \in ℕ \land N \leq M)$
18		3anan12	$⊢ (N \in ℕ \land M \in ℕ \land N \leq M) \leftrightarrow (M \in ℕ \land (N \in ℕ \land N \leq M))$
19	13 17 18	sylanbrc	$⊢ N \in (1 \dots M) \to (N \in ℕ \land M \in ℕ \land N \leq M)$
20		nnz	$⊢ M \in ℕ \to M \in ℤ$
21	20 15	syl	$⊢ M \in ℕ \to (N \in (1 \dots M) \leftrightarrow (N \in ℕ \land N \leq M))$
22	21	biimprd	$⊢ M \in ℕ \to ((N \in ℕ \land N \leq M) \to N \in (1 \dots M))$
23	22	expd	$⊢ M \in ℕ \to (N \in ℕ \to (N \leq M \to N \in (1 \dots M)))$
24	23	3imp21	$⊢ (N \in ℕ \land M \in ℕ \land N \leq M) \to N \in (1 \dots M)$
25	19 24	impbii	$⊢ N \in (1 \dots M) \leftrightarrow (N \in ℕ \land M \in ℕ \land N \leq M)$

Metamath Proof Explorer

Theorem elfz1b

Proof