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	⊢ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) → ( ( 𝑁 − 𝐿 ) − ( 𝑀 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2	⊢ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
2		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
4		zcn	⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℂ )
5	2 3 4	3anim123i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) )
6	5	3comr	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) )
7	6	adantr	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) )
8	1 7	sylbi	⊢ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) )
9		nnncan2	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝑁 − 𝐿 ) − ( 𝑀 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
10	8 9	syl	⊢ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) → ( ( 𝑁 − 𝐿 ) − ( 𝑀 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )