This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )