fzosumm1

Description: Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023)

Step	Hyp	Ref	Expression
1		fzosumm1.1	$⊢ φ \to N - 1 \in ℤ_{\geq M}$
2		fzosumm1.2	$⊢ (φ \land k \in (M ..^N)) \to A \in ℂ$
3		fzosumm1.3	$⊢ k = N - 1 \to A = B$
4		fzosumm1.n	$⊢ φ \to N \in ℤ$
5		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
6	4 5	syl	$⊢ φ \to (M ..^N) = (M \dots N - 1)$
7	6	eqcomd	$⊢ φ \to (M \dots N - 1) = (M ..^N)$
8	7	eleq2d	$⊢ φ \to (k \in (M \dots N - 1) \leftrightarrow k \in (M ..^N))$
9	8	biimpa	$⊢ (φ \land k \in (M \dots N - 1)) \to k \in (M ..^N)$
10	9 2	syldan	$⊢ (φ \land k \in (M \dots N - 1)) \to A \in ℂ$
11	1 10 3	fsumm1	$⊢ φ \to \sum_{k = M}^{N - 1} A = \sum_{k = M}^{N - 1 - 1} A + B$
12	6	sumeq1d	$⊢ φ \to \sum_{k \in (M ..^N)} A = \sum_{k = M}^{N - 1} A$
13		eluzelz	$⊢ N - 1 \in ℤ_{\geq M} \to N - 1 \in ℤ$
14		fzoval	$⊢ N - 1 \in ℤ \to (M ..^N - 1) = (M \dots N - 1 - 1)$
15	1 13 14	3syl	$⊢ φ \to (M ..^N - 1) = (M \dots N - 1 - 1)$
16	15	sumeq1d	$⊢ φ \to \sum_{k \in (M ..^N - 1)} A = \sum_{k = M}^{N - 1 - 1} A$
17	16	oveq1d	$⊢ φ \to \sum_{k \in (M ..^N - 1)} A + B = \sum_{k = M}^{N - 1 - 1} A + B$
18	11 12 17	3eqtr4d	$⊢ φ \to \sum_{k \in (M ..^N)} A = \sum_{k \in (M ..^N - 1)} A + B$

Metamath Proof Explorer