elfzo1

Description: Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017)

		Ref	Expression
	Assertion	elfzo1	$⊢ N \in (1 ..^M) \leftrightarrow (N \in ℕ \land M \in ℕ \land N < M)$

Step	Hyp	Ref	Expression
1		fzossnn	$⊢ (1 ..^M) \subseteq ℕ$
2	1	sseli	$⊢ N \in (1 ..^M) \to N \in ℕ$
3		elfzouz2	$⊢ N \in (1 ..^M) \to M \in ℤ_{\geq N}$
4		eluznn	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to M \in ℕ$
5	2 3 4	syl2anc	$⊢ N \in (1 ..^M) \to M \in ℕ$
6		elfzolt2	$⊢ N \in (1 ..^M) \to N < M$
7	2 5 6	3jca	$⊢ N \in (1 ..^M) \to (N \in ℕ \land M \in ℕ \land N < M)$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9	8	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
10	9	sseli	$⊢ N \in ℕ \to N \in ℤ_{\geq 1}$
11		nnz	$⊢ M \in ℕ \to M \in ℤ$
12		id	$⊢ N < M \to N < M$
13	10 11 12	3anim123i	$⊢ (N \in ℕ \land M \in ℕ \land N < M) \to (N \in ℤ_{\geq 1} \land M \in ℤ \land N < M)$
14		elfzo2	$⊢ N \in (1 ..^M) \leftrightarrow (N \in ℤ_{\geq 1} \land M \in ℤ \land N < M)$
15	13 14	sylibr	$⊢ (N \in ℕ \land M \in ℕ \land N < M) \to N \in (1 ..^M)$
16	7 15	impbii	$⊢ N \in (1 ..^M) \leftrightarrow (N \in ℕ \land M \in ℕ \land N < M)$

Metamath Proof Explorer