This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ L … N → N - L - M − L = N − M

Proof

Step Hyp Ref Expression
1 elfz2 ⊢ M ∈ L … N ↔ L ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ L ≤ M ∧ M ≤ N
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 zcn ⊢ M ∈ ℤ → M ∈ ℂ
4 zcn ⊢ L ∈ ℤ → L ∈ ℂ
5 2 3 4 3anim123i ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ L ∈ ℤ → N ∈ ℂ ∧ M ∈ ℂ ∧ L ∈ ℂ
6 5 3comr ⊢ L ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ → N ∈ ℂ ∧ M ∈ ℂ ∧ L ∈ ℂ
7 6 adantr ⊢ L ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ L ≤ M ∧ M ≤ N → N ∈ ℂ ∧ M ∈ ℂ ∧ L ∈ ℂ
8 1 7 sylbi ⊢ M ∈ L … N → N ∈ ℂ ∧ M ∈ ℂ ∧ L ∈ ℂ
9 nnncan2 ⊢ N ∈ ℂ ∧ M ∈ ℂ ∧ L ∈ ℂ → N - L - M − L = N − M
10 8 9 syl ⊢ M ∈ L … N → N - L - M − L = N − M