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 )
12 11 adantr 
 |-  ( ( K e. ZZ /\ M e. NN0 ) -> K e. RR )
13 5 adantl 
 |-  ( ( 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 ) )
20 19 adantl 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 ) )