fsump1i

Description: Optimized version of fsump1 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014)

Step	Hyp	Ref	Expression
1		fsump1i.1	$⊢ Z = ℤ_{\geq M}$
2		fsump1i.2	$⊢ N = K + 1$
3		fsump1i.3	$⊢ k = N \to A = B$
4		fsump1i.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		fsump1i.5	$⊢ φ \to (K \in Z \land \sum_{k = M}^{K} A = S)$
6		fsump1i.6	$⊢ φ \to S + B = T$
7	5	simpld	$⊢ φ \to K \in Z$
8	7 1	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq M}$
9		peano2uz	$⊢ K \in ℤ_{\geq M} \to K + 1 \in ℤ_{\geq M}$
10	9 1	eleqtrrdi	$⊢ K \in ℤ_{\geq M} \to K + 1 \in Z$
11	8 10	syl	$⊢ φ \to K + 1 \in Z$
12	2 11	eqeltrid	$⊢ φ \to N \in Z$
13	2	oveq2i	$⊢ (M \dots N) = (M \dots K + 1)$
14	13	sumeq1i	$⊢ \sum_{k = M}^{N} A = \sum_{k = M}^{K + 1} A$
15		elfzuz	$⊢ k \in (M \dots K + 1) \to k \in ℤ_{\geq M}$
16	15 1	eleqtrrdi	$⊢ k \in (M \dots K + 1) \to k \in Z$
17	16 4	sylan2	$⊢ (φ \land k \in (M \dots K + 1)) \to A \in ℂ$
18	2	eqeq2i	$⊢ k = N \leftrightarrow k = K + 1$
19	18 3	sylbir	$⊢ k = K + 1 \to A = B$
20	8 17 19	fsump1	$⊢ φ \to \sum_{k = M}^{K + 1} A = \sum_{k = M}^{K} A + B$
21	14 20	eqtrid	$⊢ φ \to \sum_{k = M}^{N} A = \sum_{k = M}^{K} A + B$
22	5	simprd	$⊢ φ \to \sum_{k = M}^{K} A = S$
23	22	oveq1d	$⊢ φ \to \sum_{k = M}^{K} A + B = S + B$
24	21 23 6	3eqtrd	$⊢ φ \to \sum_{k = M}^{N} A = T$
25	12 24	jca	$⊢ φ \to (N \in Z \land \sum_{k = M}^{N} A = T)$

Metamath Proof Explorer