fsumsermpt

Description: A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	fsumsermpt.m	$⊢ φ \to M \in ℤ$
	fsumsermpt.z	$⊢ Z = ℤ_{\geq M}$
	fsumsermpt.a	$⊢ (φ \land k \in Z) \to A \in ℂ$
	fsumsermpt.f	$⊢ F = (n \in Z ⟼ \sum_{k = M}^{n} A)$
	fsumsermpt.g	$⊢ G = seq M (+ (k \in Z ⟼ A))$
Assertion	fsumsermpt	$⊢ φ \to F = G$

Proof

Step	Hyp	Ref	Expression
1		fsumsermpt.m	$⊢ φ \to M \in ℤ$
2		fsumsermpt.z	$⊢ Z = ℤ_{\geq M}$
3		fsumsermpt.a	$⊢ (φ \land k \in Z) \to A \in ℂ$
4		fsumsermpt.f	$⊢ F = (n \in Z ⟼ \sum_{k = M}^{n} A)$
5		fsumsermpt.g	$⊢ G = seq M (+ (k \in Z ⟼ A))$
6		fzfid	$⊢ φ \to (M \dots m) \in Fin$
7		simpl	$⊢ (φ \land k \in (M \dots m)) \to φ$
8		elfzuz	$⊢ k \in (M \dots m) \to k \in ℤ_{\geq M}$
9	8 2	eleqtrrdi	$⊢ k \in (M \dots m) \to k \in Z$
10	9	adantl	$⊢ (φ \land k \in (M \dots m)) \to k \in Z$
11	7 10 3	syl2anc	$⊢ (φ \land k \in (M \dots m)) \to A \in ℂ$
12	6 11	fsumcl	$⊢ φ \to \sum_{k = M}^{m} A \in ℂ$
13	12	adantr	$⊢ (φ \land m \in Z) \to \sum_{k = M}^{m} A \in ℂ$
14	13	ralrimiva	$⊢ φ \to \forall m \in Z \sum_{k = M}^{m} A \in ℂ$
15		oveq2	$⊢ n = m \to (M \dots n) = (M \dots m)$
16	15	sumeq1d	$⊢ n = m \to \sum_{k = M}^{n} A = \sum_{k = M}^{m} A$
17	16	cbvmptv	$⊢ (n \in Z ⟼ \sum_{k = M}^{n} A) = (m \in Z ⟼ \sum_{k = M}^{m} A)$
18	4 17	eqtri	$⊢ F = (m \in Z ⟼ \sum_{k = M}^{m} A)$
19	18	fnmpt	$⊢ \forall m \in Z \sum_{k = M}^{m} A \in ℂ \to F Fn Z$
20	14 19	syl	$⊢ φ \to F Fn Z$
21		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
22		nfv	$⊢ Ⅎ k (φ \land j \in Z)$
23		nfcv	$⊢ \underline{Ⅎ} k j$
24	23	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
25	24	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ A \in ℂ$
26	22 25	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ)$
27		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
28	27	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
29		csbeq1a	$⊢ k = j \to A = ⦋ j / k ⦌ A$
30	29	eleq1d	$⊢ k = j \to (A \in ℂ \leftrightarrow ⦋ j / k ⦌ A \in ℂ)$
31	28 30	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to A \in ℂ) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ))$
32	26 31 3	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ A \in ℂ$
33		eqid	$⊢ (k \in Z ⟼ A) = (k \in Z ⟼ A)$
34	23 24 29 33	fvmptf	$⊢ (j \in Z \land ⦋ j / k ⦌ A \in ℂ) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
35	21 32 34	syl2anc	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
36	35 32	eqeltrd	$⊢ (φ \land j \in Z) \to (k \in Z ⟼ A) (j) \in ℂ$
37		addcl	$⊢ (j \in ℂ \land x \in ℂ) \to j + x \in ℂ$
38	37	adantl	$⊢ (φ \land (j \in ℂ \land x \in ℂ)) \to j + x \in ℂ$
39	2 1 36 38	seqf	$⊢ φ \to seq M (+ (k \in Z ⟼ A)) : Z ⟶ ℂ$
40	39	ffnd	$⊢ φ \to seq M (+ (k \in Z ⟼ A)) Fn Z$
41	5	a1i	$⊢ φ \to G = seq M (+ (k \in Z ⟼ A))$
42	41	fneq1d	$⊢ φ \to (G Fn Z \leftrightarrow seq M (+ (k \in Z ⟼ A)) Fn Z)$
43	40 42	mpbird	$⊢ φ \to G Fn Z$
44		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
45	18	fvmpt2	$⊢ (m \in Z \land \sum_{k = M}^{m} A \in ℂ) \to F (m) = \sum_{k = M}^{m} A$
46	44 13 45	syl2anc	$⊢ (φ \land m \in Z) \to F (m) = \sum_{k = M}^{m} A$
47		nfcv	$⊢ \underline{Ⅎ} j A$
48	29 47 24	cbvsum	$⊢ \sum_{k = M}^{m} A = \sum_{j = M}^{m} ⦋ j / k ⦌ A$
49	48	a1i	$⊢ (φ \land m \in Z) \to \sum_{k = M}^{m} A = \sum_{j = M}^{m} ⦋ j / k ⦌ A$
50	46 49	eqtrd	$⊢ (φ \land m \in Z) \to F (m) = \sum_{j = M}^{m} ⦋ j / k ⦌ A$
51		simpl	$⊢ (φ \land j \in (M \dots m)) \to φ$
52		elfzuz	$⊢ j \in (M \dots m) \to j \in ℤ_{\geq M}$
53	52 2	eleqtrrdi	$⊢ j \in (M \dots m) \to j \in Z$
54	53	adantl	$⊢ (φ \land j \in (M \dots m)) \to j \in Z$
55	51 54 35	syl2anc	$⊢ (φ \land j \in (M \dots m)) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
56	55	adantlr	$⊢ ((φ \land m \in Z) \land j \in (M \dots m)) \to (k \in Z ⟼ A) (j) = ⦋ j / k ⦌ A$
57		id	$⊢ m \in Z \to m \in Z$
58	57 2	eleqtrdi	$⊢ m \in Z \to m \in ℤ_{\geq M}$
59	58	adantl	$⊢ (φ \land m \in Z) \to m \in ℤ_{\geq M}$
60	51 54 32	syl2anc	$⊢ (φ \land j \in (M \dots m)) \to ⦋ j / k ⦌ A \in ℂ$
61	60	adantlr	$⊢ ((φ \land m \in Z) \land j \in (M \dots m)) \to ⦋ j / k ⦌ A \in ℂ$
62	56 59 61	fsumser	$⊢ (φ \land m \in Z) \to \sum_{j = M}^{m} ⦋ j / k ⦌ A = seq M (+ (k \in Z ⟼ A)) (m)$
63	5	fveq1i	$⊢ G (m) = seq M (+ (k \in Z ⟼ A)) (m)$
64	63	eqcomi	$⊢ seq M (+ (k \in Z ⟼ A)) (m) = G (m)$
65	64	a1i	$⊢ (φ \land m \in Z) \to seq M (+ (k \in Z ⟼ A)) (m) = G (m)$
66	50 62 65	3eqtrd	$⊢ (φ \land m \in Z) \to F (m) = G (m)$
67	20 43 66	eqfnfvd	$⊢ φ \to F = G$

Metamath Proof Explorer

Theorem fsumsermpt

Proof