Metamath Proof Explorer

Theorem fzmmmeqm

Description: Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range results in the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018)

Ref Expression
Assertion fzmmmeqm 
|- ( M e. ( L ... N ) -> ( ( N - L ) - ( M - L ) ) = ( N - M ) )

Proof

Step Hyp Ref Expression
1 elfz2 
 |-  ( M e. ( L ... N ) <-> ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) )
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 zcn 
 |-  ( M e. ZZ -> M e. CC )
4 zcn 
 |-  ( L e. ZZ -> L e. CC )
5 2 3 4 3anim123i 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ L e. ZZ ) -> ( N e. CC /\ M e. CC /\ L e. CC ) )
6 5 3comr 
 |-  ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( N e. CC /\ M e. CC /\ L e. CC ) )
7 6 adantr 
 |-  ( ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) -> ( N e. CC /\ M e. CC /\ L e. CC ) )
8 1 7 sylbi 
 |-  ( M e. ( L ... N ) -> ( N e. CC /\ M e. CC /\ L e. CC ) )
9 nnncan2 
 |-  ( ( N e. CC /\ M e. CC /\ L e. CC ) -> ( ( N - L ) - ( M - L ) ) = ( N - M ) )
10 8 9 syl 
 |-  ( M e. ( L ... N ) -> ( ( N - L ) - ( M - L ) ) = ( N - M ) )