fzo1fzo0n0

Description: An integer between 1 and an upper bound of a half-open integer range is not 0 and between 0 and the upper bound of the half-open integer range. (Contributed by Alexander van der Vekens, 21-Mar-2018)

		Ref	Expression
	Assertion	fzo1fzo0n0	$⊢ K \in (1 ..^N) \leftrightarrow (K \in (0 ..^N) \land K \neq 0)$

Proof

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ K \in (1 ..^N) \leftrightarrow (K \in ℤ_{\geq 1} \land N \in ℤ \land K < N)$
2		elnnuz	$⊢ K \in ℕ \leftrightarrow K \in ℤ_{\geq 1}$
3		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
4	3	adantr	$⊢ (K \in ℕ \land N \in ℤ) \to K \in ℕ_{0}$
5	4	adantr	$⊢ ((K \in ℕ \land N \in ℤ) \land K < N) \to K \in ℕ_{0}$
6		nngt0	$⊢ K \in ℕ \to 0 < K$
7		0red	$⊢ (N \in ℤ \land K \in ℕ) \to 0 \in ℝ$
8		nnre	$⊢ K \in ℕ \to K \in ℝ$
9	8	adantl	$⊢ (N \in ℤ \land K \in ℕ) \to K \in ℝ$
10		zre	$⊢ N \in ℤ \to N \in ℝ$
11	10	adantr	$⊢ (N \in ℤ \land K \in ℕ) \to N \in ℝ$
12		lttr	$⊢ (0 \in ℝ \land K \in ℝ \land N \in ℝ) \to ((0 < K \land K < N) \to 0 < N)$
13	7 9 11 12	syl3anc	$⊢ (N \in ℤ \land K \in ℕ) \to ((0 < K \land K < N) \to 0 < N)$
14		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
15	14	simplbi2	$⊢ N \in ℤ \to (0 < N \to N \in ℕ)$
16	15	adantr	$⊢ (N \in ℤ \land K \in ℕ) \to (0 < N \to N \in ℕ)$
17	13 16	syld	$⊢ (N \in ℤ \land K \in ℕ) \to ((0 < K \land K < N) \to N \in ℕ)$
18	17	exp4b	$⊢ N \in ℤ \to (K \in ℕ \to (0 < K \to (K < N \to N \in ℕ)))$
19	18	com13	$⊢ 0 < K \to (K \in ℕ \to (N \in ℤ \to (K < N \to N \in ℕ)))$
20	6 19	mpcom	$⊢ K \in ℕ \to (N \in ℤ \to (K < N \to N \in ℕ))$
21	20	imp31	$⊢ ((K \in ℕ \land N \in ℤ) \land K < N) \to N \in ℕ$
22		simpr	$⊢ ((K \in ℕ \land N \in ℤ) \land K < N) \to K < N$
23	5 21 22	3jca	$⊢ ((K \in ℕ \land N \in ℤ) \land K < N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
24	23	exp31	$⊢ K \in ℕ \to (N \in ℤ \to (K < N \to (K \in ℕ_{0} \land N \in ℕ \land K < N)))$
25	2 24	sylbir	$⊢ K \in ℤ_{\geq 1} \to (N \in ℤ \to (K < N \to (K \in ℕ_{0} \land N \in ℕ \land K < N)))$
26	25	3imp	$⊢ (K \in ℤ_{\geq 1} \land N \in ℤ \land K < N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
27		elfzo0	$⊢ K \in (0 ..^N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ \land K < N)$
28	26 27	sylibr	$⊢ (K \in ℤ_{\geq 1} \land N \in ℤ \land K < N) \to K \in (0 ..^N)$
29		nnne0	$⊢ K \in ℕ \to K \neq 0$
30	2 29	sylbir	$⊢ K \in ℤ_{\geq 1} \to K \neq 0$
31	30	3ad2ant1	$⊢ (K \in ℤ_{\geq 1} \land N \in ℤ \land K < N) \to K \neq 0$
32	28 31	jca	$⊢ (K \in ℤ_{\geq 1} \land N \in ℤ \land K < N) \to (K \in (0 ..^N) \land K \neq 0)$
33	1 32	sylbi	$⊢ K \in (1 ..^N) \to (K \in (0 ..^N) \land K \neq 0)$
34		elnnne0	$⊢ K \in ℕ \leftrightarrow (K \in ℕ_{0} \land K \neq 0)$
35		nnge1	$⊢ K \in ℕ \to 1 \leq K$
36	34 35	sylbir	$⊢ (K \in ℕ_{0} \land K \neq 0) \to 1 \leq K$
37	36	3ad2antl1	$⊢ ((K \in ℕ_{0} \land N \in ℕ \land K < N) \land K \neq 0) \to 1 \leq K$
38		simpl3	$⊢ ((K \in ℕ_{0} \land N \in ℕ \land K < N) \land K \neq 0) \to K < N$
39		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
40	39	adantr	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to K \in ℤ$
41		1zzd	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to 1 \in ℤ$
42		nnz	$⊢ N \in ℕ \to N \in ℤ$
43	42	adantl	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to N \in ℤ$
44	40 41 43	3jca	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (K \in ℤ \land 1 \in ℤ \land N \in ℤ)$
45	44	3adant3	$⊢ (K \in ℕ_{0} \land N \in ℕ \land K < N) \to (K \in ℤ \land 1 \in ℤ \land N \in ℤ)$
46	45	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ \land K < N) \land K \neq 0) \to (K \in ℤ \land 1 \in ℤ \land N \in ℤ)$
47		elfzo	$⊢ (K \in ℤ \land 1 \in ℤ \land N \in ℤ) \to (K \in (1 ..^N) \leftrightarrow (1 \leq K \land K < N))$
48	46 47	syl	$⊢ ((K \in ℕ_{0} \land N \in ℕ \land K < N) \land K \neq 0) \to (K \in (1 ..^N) \leftrightarrow (1 \leq K \land K < N))$
49	37 38 48	mpbir2and	$⊢ ((K \in ℕ_{0} \land N \in ℕ \land K < N) \land K \neq 0) \to K \in (1 ..^N)$
50	27 49	sylanb	$⊢ (K \in (0 ..^N) \land K \neq 0) \to K \in (1 ..^N)$
51	33 50	impbii	$⊢ K \in (1 ..^N) \leftrightarrow (K \in (0 ..^N) \land K \neq 0)$

Metamath Proof Explorer

Theorem fzo1fzo0n0

Proof