# 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
`|- ( ( K =/= M /\ K e. ( 0 ... M ) ) -> K e. ( 0 ..^ M ) )`

### Proof

Step Hyp Ref Expression
1 elfz2nn0
` |-  ( K e. ( 0 ... M ) <-> ( K e. NN0 /\ M e. NN0 /\ K <_ M ) )`
2 simpl1
` |-  ( ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) /\ K =/= M ) -> K e. NN0 )`
3 necom
` |-  ( K =/= M <-> M =/= K )`
4 nn0re
` |-  ( K e. NN0 -> K e. RR )`
5 nn0re
` |-  ( M e. NN0 -> M e. RR )`
6 ltlen
` |-  ( ( K e. RR /\ M e. RR ) -> ( K < M <-> ( K <_ M /\ M =/= K ) ) )`
7 4 5 6 syl2an
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K < M <-> ( K <_ M /\ M =/= K ) ) )`
8 7 bicomd
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( K <_ M /\ M =/= K ) <-> K < M ) )`
9 elnn0z
` |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )`
10 0red
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> 0 e. RR )`
11 zre
` |-  ( K e. ZZ -> K e. RR )`
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> K e. RR )`
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> M e. RR )`
14 lelttr
` |-  ( ( 0 e. RR /\ K e. RR /\ M e. RR ) -> ( ( 0 <_ K /\ K < M ) -> 0 < M ) )`
15 10 12 13 14 syl3anc
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> ( ( 0 <_ K /\ K < M ) -> 0 < M ) )`
16 nn0z
` |-  ( M e. NN0 -> M e. ZZ )`
17 elnnz
` |-  ( M e. NN <-> ( M e. ZZ /\ 0 < M ) )`
18 17 simplbi2
` |-  ( M e. ZZ -> ( 0 < M -> M e. NN ) )`
19 16 18 syl
` |-  ( M e. NN0 -> ( 0 < M -> M e. NN ) )`
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> ( 0 < M -> M e. NN ) )`
21 15 20 syld
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> ( ( 0 <_ K /\ K < M ) -> M e. NN ) )`
22 21 expd
` |-  ( ( K e. ZZ /\ M e. NN0 ) -> ( 0 <_ K -> ( K < M -> M e. NN ) ) )`
23 22 impancom
` |-  ( ( K e. ZZ /\ 0 <_ K ) -> ( M e. NN0 -> ( K < M -> M e. NN ) ) )`
24 9 23 sylbi
` |-  ( K e. NN0 -> ( M e. NN0 -> ( K < M -> M e. NN ) ) )`
25 24 imp
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K < M -> M e. NN ) )`
26 8 25 sylbid
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( K <_ M /\ M =/= K ) -> M e. NN ) )`
27 26 expd
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K <_ M -> ( M =/= K -> M e. NN ) ) )`
28 3 27 syl7bi
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K <_ M -> ( K =/= M -> M e. NN ) ) )`
29 28 3impia
` |-  ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) -> ( K =/= M -> M e. NN ) )`
30 29 imp
` |-  ( ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) /\ K =/= M ) -> M e. NN )`
31 8 biimpd
` |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( K <_ M /\ M =/= K ) -> K < M ) )`
32 31 exp4b
` |-  ( K e. NN0 -> ( M e. NN0 -> ( K <_ M -> ( M =/= K -> K < M ) ) ) )`
33 32 3imp
` |-  ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) -> ( M =/= K -> K < M ) )`
34 3 33 syl5bi
` |-  ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) -> ( K =/= M -> K < M ) )`
35 34 imp
` |-  ( ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) /\ K =/= M ) -> K < M )`
36 2 30 35 3jca
` |-  ( ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) /\ K =/= M ) -> ( K e. NN0 /\ M e. NN /\ K < M ) )`
37 36 ex
` |-  ( ( K e. NN0 /\ M e. NN0 /\ K <_ M ) -> ( K =/= M -> ( K e. NN0 /\ M e. NN /\ K < M ) ) )`
38 1 37 sylbi
` |-  ( K e. ( 0 ... M ) -> ( K =/= M -> ( K e. NN0 /\ M e. NN /\ K < M ) ) )`
39 38 impcom
` |-  ( ( K =/= M /\ K e. ( 0 ... M ) ) -> ( K e. NN0 /\ M e. NN /\ K < M ) )`
40 elfzo0
` |-  ( K e. ( 0 ..^ M ) <-> ( K e. NN0 /\ M e. NN /\ K < M ) )`
41 39 40 sylibr
` |-  ( ( K =/= M /\ K e. ( 0 ... M ) ) -> K e. ( 0 ..^ M ) )`