Metamath Proof Explorer

Theorem elfzmlbm

Description: Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion elfzmlbm 
|- ( K e. ( M ... N ) -> ( K - M ) e. ( 0 ... ( N - M ) ) )

Proof

Step Hyp Ref Expression
1 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2 uznn0sub 
 |-  ( K e. ( ZZ>= ` M ) -> ( K - M ) e. NN0 )
3 1 2 syl 
 |-  ( K e. ( M ... N ) -> ( K - M ) e. NN0 )
4 elfzuz2 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
5 uznn0sub 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
6 4 5 syl 
 |-  ( K e. ( M ... N ) -> ( N - M ) e. NN0 )
7 elfzelz 
 |-  ( K e. ( M ... N ) -> K e. ZZ )
8 7 zred 
 |-  ( K e. ( M ... N ) -> K e. RR )
9 elfzel2 
 |-  ( K e. ( M ... N ) -> N e. ZZ )
10 9 zred 
 |-  ( K e. ( M ... N ) -> N e. RR )
11 elfzel1 
 |-  ( K e. ( M ... N ) -> M e. ZZ )
12 11 zred 
 |-  ( K e. ( M ... N ) -> M e. RR )
13 elfzle2 
 |-  ( K e. ( M ... N ) -> K <_ N )
14 8 10 12 13 lesub1dd 
 |-  ( K e. ( M ... N ) -> ( K - M ) <_ ( N - M ) )
15 elfz2nn0 
 |-  ( ( K - M ) e. ( 0 ... ( N - M ) ) <-> ( ( K - M ) e. NN0 /\ ( N - M ) e. NN0 /\ ( K - M ) <_ ( N - M ) ) )
16 3 6 14 15 syl3anbrc 
 |-  ( K e. ( M ... N ) -> ( K - M ) e. ( 0 ... ( N - M ) ) )