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

Metamath Proof Explorer

Theorem fzofzim

Description: If a nonnegative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open integer range. (Contributed by Alexander van der Vekens, 15-Jun-2018)

Ref Expression
Assertion fzofzim ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → 𝐾 ∈ ( 0 ..^ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑀 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) )
2 simpl1 ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℕ0 )
3 necom ⊢ ( 𝐾 ≠ 𝑀 ↔ 𝑀 ≠ 𝐾 )
4 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
5 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
6 ltlen ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐾 < 𝑀 ↔ ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ) )
7 4 5 6 syl2an ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 < 𝑀 ↔ ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ) )
8 7 bicomd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ↔ 𝐾 < 𝑀 ) )
9 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
10 0red ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ∈ ℝ )
11 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝐾 ∈ ℝ )
13 5 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
14 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 0 < 𝑀 ) )
15 10 12 13 14 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 0 < 𝑀 ) )
16 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
17 elnnz ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
18 17 simplbi2 ⊢ ( 𝑀 ∈ ℤ → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
19 16 18 syl ⊢ ( 𝑀 ∈ ℕ0 → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
20 19 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
21 15 20 syld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 𝑀 ∈ ℕ ) )
22 21 expd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ 𝐾 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
23 22 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
24 9 23 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
25 24 imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) )
26 8 25 sylbid ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) → 𝑀 ∈ ℕ ) )
27 26 expd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑀 → ( 𝑀 ≠ 𝐾 → 𝑀 ∈ ℕ ) ) )
28 3 27 syl7bi ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑀 → ( 𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ ) ) )
29 28 3impia ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ ) )
30 29 imp ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℕ )
31 8 biimpd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) → 𝐾 < 𝑀 ) )
32 31 exp4b ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑀 → ( 𝑀 ≠ 𝐾 → 𝐾 < 𝑀 ) ) ) )
33 32 3imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 ≠ 𝐾 → 𝐾 < 𝑀 ) )
34 3 33 biimtrid ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → 𝐾 < 𝑀 ) )
35 34 imp ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 < 𝑀 )
36 2 30 35 3jca ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
37 36 ex ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) ) )
38 1 37 sylbi ⊢ ( 𝐾 ∈ ( 0 ... 𝑀 ) → ( 𝐾 ≠ 𝑀 → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) ) )
39 38 impcom ⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
40 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
41 39 40 sylibr ⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → 𝐾 ∈ ( 0 ..^ 𝑀 ) )