Theorem 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	⊢ ( 𝐾 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ≠ 0 ) )

Proof

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