# 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 ${⊢}\left({K}\ne {M}\wedge {K}\in \left(0\dots {M}\right)\right)\to {K}\in \left(0..^{M}\right)$

### Proof

Step Hyp Ref Expression
1 elfz2nn0 ${⊢}{K}\in \left(0\dots {M}\right)↔\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)$
2 simpl1 ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\wedge {K}\ne {M}\right)\to {K}\in {ℕ}_{0}$
3 necom ${⊢}{K}\ne {M}↔{M}\ne {K}$
4 nn0re ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℝ$
5 nn0re ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℝ$
6 ltlen ${⊢}\left({K}\in ℝ\wedge {M}\in ℝ\right)\to \left({K}<{M}↔\left({K}\le {M}\wedge {M}\ne {K}\right)\right)$
7 4 5 6 syl2an ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({K}<{M}↔\left({K}\le {M}\wedge {M}\ne {K}\right)\right)$
8 7 bicomd ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left(\left({K}\le {M}\wedge {M}\ne {K}\right)↔{K}<{M}\right)$
9 elnn0z ${⊢}{K}\in {ℕ}_{0}↔\left({K}\in ℤ\wedge 0\le {K}\right)$
10 0red ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to 0\in ℝ$
11 zre ${⊢}{K}\in ℤ\to {K}\in ℝ$
12 11 adantr ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to {K}\in ℝ$
13 5 adantl ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to {M}\in ℝ$
14 lelttr ${⊢}\left(0\in ℝ\wedge {K}\in ℝ\wedge {M}\in ℝ\right)\to \left(\left(0\le {K}\wedge {K}<{M}\right)\to 0<{M}\right)$
15 10 12 13 14 syl3anc ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left(\left(0\le {K}\wedge {K}<{M}\right)\to 0<{M}\right)$
16 nn0z ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℤ$
17 elnnz ${⊢}{M}\in ℕ↔\left({M}\in ℤ\wedge 0<{M}\right)$
18 17 simplbi2 ${⊢}{M}\in ℤ\to \left(0<{M}\to {M}\in ℕ\right)$
19 16 18 syl ${⊢}{M}\in {ℕ}_{0}\to \left(0<{M}\to {M}\in ℕ\right)$
20 19 adantl ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left(0<{M}\to {M}\in ℕ\right)$
21 15 20 syld ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left(\left(0\le {K}\wedge {K}<{M}\right)\to {M}\in ℕ\right)$
22 21 expd ${⊢}\left({K}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left(0\le {K}\to \left({K}<{M}\to {M}\in ℕ\right)\right)$
23 22 impancom ${⊢}\left({K}\in ℤ\wedge 0\le {K}\right)\to \left({M}\in {ℕ}_{0}\to \left({K}<{M}\to {M}\in ℕ\right)\right)$
24 9 23 sylbi ${⊢}{K}\in {ℕ}_{0}\to \left({M}\in {ℕ}_{0}\to \left({K}<{M}\to {M}\in ℕ\right)\right)$
25 24 imp ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({K}<{M}\to {M}\in ℕ\right)$
26 8 25 sylbid ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left(\left({K}\le {M}\wedge {M}\ne {K}\right)\to {M}\in ℕ\right)$
27 26 expd ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({K}\le {M}\to \left({M}\ne {K}\to {M}\in ℕ\right)\right)$
28 3 27 syl7bi ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left({K}\le {M}\to \left({K}\ne {M}\to {M}\in ℕ\right)\right)$
29 28 3impia ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\to \left({K}\ne {M}\to {M}\in ℕ\right)$
30 29 imp ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\wedge {K}\ne {M}\right)\to {M}\in ℕ$
31 8 biimpd ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left(\left({K}\le {M}\wedge {M}\ne {K}\right)\to {K}<{M}\right)$
32 31 exp4b ${⊢}{K}\in {ℕ}_{0}\to \left({M}\in {ℕ}_{0}\to \left({K}\le {M}\to \left({M}\ne {K}\to {K}<{M}\right)\right)\right)$
33 32 3imp ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\to \left({M}\ne {K}\to {K}<{M}\right)$
34 3 33 syl5bi ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\to \left({K}\ne {M}\to {K}<{M}\right)$
35 34 imp ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\wedge {K}\ne {M}\right)\to {K}<{M}$
36 2 30 35 3jca ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\wedge {K}\ne {M}\right)\to \left({K}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {K}<{M}\right)$
37 36 ex ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {K}\le {M}\right)\to \left({K}\ne {M}\to \left({K}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {K}<{M}\right)\right)$
38 1 37 sylbi ${⊢}{K}\in \left(0\dots {M}\right)\to \left({K}\ne {M}\to \left({K}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {K}<{M}\right)\right)$
39 38 impcom ${⊢}\left({K}\ne {M}\wedge {K}\in \left(0\dots {M}\right)\right)\to \left({K}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {K}<{M}\right)$
40 elfzo0 ${⊢}{K}\in \left(0..^{M}\right)↔\left({K}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {K}<{M}\right)$
41 39 40 sylibr ${⊢}\left({K}\ne {M}\wedge {K}\in \left(0\dots {M}\right)\right)\to {K}\in \left(0..^{M}\right)$