fsum

Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014) (Revised by Mario Carneiro, 13-Jun-2019)

	Ref	Expression
Hypotheses	fsum.1	$⊢ k = F (n) \to B = C$
	fsum.2	$⊢ φ \to M \in ℕ$
	fsum.3	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} A$
	fsum.4	$⊢ (φ \land k \in A) \to B \in ℂ$
	fsum.5	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = C$
Assertion	fsum	$⊢ φ \to \sum_{k \in A} B = seq 1 (+ G) (M)$

Proof

Step	Hyp	Ref	Expression
1		fsum.1	$⊢ k = F (n) \to B = C$
2		fsum.2	$⊢ φ \to M \in ℕ$
3		fsum.3	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} A$
4		fsum.4	$⊢ (φ \land k \in A) \to B \in ℂ$
5		fsum.5	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = C$
6		df-sum	$⊢ \sum_{k \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
7		fvex	$⊢ seq 1 (+ G) (M) \in V$
8		eleq1w	$⊢ n = j \to (n \in A \leftrightarrow j \in A)$
9		csbeq1	$⊢ n = j \to ⦋ n / k ⦌ B = ⦋ j / k ⦌ B$
10	8 9	ifbieq1d	$⊢ n = j \to if (n \in A, ⦋ n / k ⦌ B, 0) = if (j \in A, ⦋ j / k ⦌ B, 0)$
11	10	cbvmptv	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) = (j \in ℤ ⟼ if (j \in A, ⦋ j / k ⦌ B, 0))$
12	4	ralrimiva	$⊢ φ \to \forall k \in A B \in ℂ$
13		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
14	13	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℂ$
15		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
16	15	eleq1d	$⊢ k = j \to (B \in ℂ \leftrightarrow ⦋ j / k ⦌ B \in ℂ)$
17	14 16	rspc	$⊢ j \in A \to (\forall k \in A B \in ℂ \to ⦋ j / k ⦌ B \in ℂ)$
18	12 17	mpan9	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in ℂ$
19		fveq2	$⊢ n = i \to f (n) = f (i)$
20	19	csbeq1d	$⊢ n = i \to ⦋ f (n) / k ⦌ B = ⦋ f (i) / k ⦌ B$
21		csbcow	$⊢ ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B = ⦋ f (i) / k ⦌ B$
22	20 21	eqtr4di	$⊢ n = i \to ⦋ f (n) / k ⦌ B = ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B$
23	22	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (i \in ℕ ⟼ ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B)$
24	11 18 23	summo	$⊢ φ \to \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
25		f1of	$⊢ F : (1 \dots M) \underset{1-1 onto}{⟶} A \to F : (1 \dots M) ⟶ A$
26	3 25	syl	$⊢ φ \to F : (1 \dots M) ⟶ A$
27		ovex	$⊢ (1 \dots M) \in V$
28		fex	$⊢ (F : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to F \in V$
29	26 27 28	sylancl	$⊢ φ \to F \in V$
30		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
31	2 30	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
32		elfznn	$⊢ n \in (1 \dots M) \to n \in ℕ$
33		fvex	$⊢ G (n) \in V$
34	5 33	eqeltrrdi	$⊢ (φ \land n \in (1 \dots M)) \to C \in V$
35		eqid	$⊢ (n \in ℕ ⟼ C) = (n \in ℕ ⟼ C)$
36	35	fvmpt2	$⊢ (n \in ℕ \land C \in V) \to (n \in ℕ ⟼ C) (n) = C$
37	32 34 36	syl2an2	$⊢ (φ \land n \in (1 \dots M)) \to (n \in ℕ ⟼ C) (n) = C$
38	5 37	eqtr4d	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = (n \in ℕ ⟼ C) (n)$
39	38	ralrimiva	$⊢ φ \to \forall n \in (1 \dots M) G (n) = (n \in ℕ ⟼ C) (n)$
40		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ C) (k)$
41	40	nfeq2	$⊢ Ⅎ n G (k) = (n \in ℕ ⟼ C) (k)$
42		fveq2	$⊢ n = k \to G (n) = G (k)$
43		fveq2	$⊢ n = k \to (n \in ℕ ⟼ C) (n) = (n \in ℕ ⟼ C) (k)$
44	42 43	eqeq12d	$⊢ n = k \to (G (n) = (n \in ℕ ⟼ C) (n) \leftrightarrow G (k) = (n \in ℕ ⟼ C) (k))$
45	41 44	rspc	$⊢ k \in (1 \dots M) \to (\forall n \in (1 \dots M) G (n) = (n \in ℕ ⟼ C) (n) \to G (k) = (n \in ℕ ⟼ C) (k))$
46	39 45	mpan9	$⊢ (φ \land k \in (1 \dots M)) \to G (k) = (n \in ℕ ⟼ C) (k)$
47	31 46	seqfveq	$⊢ φ \to seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ C)) (M)$
48	3 47	jca	$⊢ φ \to (F : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ C)) (M))$
49		f1oeq1	$⊢ f = F \to (f : (1 \dots M) \underset{1-1 onto}{⟶} A \leftrightarrow F : (1 \dots M) \underset{1-1 onto}{⟶} A)$
50		fveq1	$⊢ f = F \to f (n) = F (n)$
51	50	csbeq1d	$⊢ f = F \to ⦋ f (n) / k ⦌ B = ⦋ F (n) / k ⦌ B$
52		fvex	$⊢ F (n) \in V$
53	52 1	csbie	$⊢ ⦋ F (n) / k ⦌ B = C$
54	51 53	syl6eq	$⊢ f = F \to ⦋ f (n) / k ⦌ B = C$
55	54	mpteq2dv	$⊢ f = F \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ C)$
56	55	seqeq3d	$⊢ f = F \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) = seq 1 (+ (n \in ℕ ⟼ C))$
57	56	fveq1d	$⊢ f = F \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M) = seq 1 (+ (n \in ℕ ⟼ C)) (M)$
58	57	eqeq2d	$⊢ f = F \to (seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M) \leftrightarrow seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ C)) (M))$
59	49 58	anbi12d	$⊢ f = F \to ((f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)) \leftrightarrow (F : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ C)) (M)))$
60	29 48 59	spcedv	$⊢ φ \to \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))$
61		oveq2	$⊢ m = M \to (1 \dots m) = (1 \dots M)$
62	61	f1oeq2d	$⊢ m = M \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots M) \underset{1-1 onto}{⟶} A)$
63		fveq2	$⊢ m = M \to seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)$
64	63	eqeq2d	$⊢ m = M \to (seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))$
65	62 64	anbi12d	$⊢ m = M \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)))$
66	65	exbidv	$⊢ m = M \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)))$
67	66	rspcev	$⊢ (M \in ℕ \land \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))) \to \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
68	2 60 67	syl2anc	$⊢ φ \to \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
69	68	olcd	$⊢ φ \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
70		breq2	$⊢ x = seq 1 (+ G) (M) \to (seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x \leftrightarrow seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M))$
71	70	anbi2d	$⊢ x = seq 1 (+ G) (M) \to ((A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)))$
72	71	rexbidv	$⊢ x = seq 1 (+ G) (M) \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \leftrightarrow \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)))$
73		eqeq1	$⊢ x = seq 1 (+ G) (M) \to (x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
74	73	anbi2d	$⊢ x = seq 1 (+ G) (M) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
75	74	exbidv	$⊢ x = seq 1 (+ G) (M) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
76	75	rexbidv	$⊢ x = seq 1 (+ G) (M) \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
77	72 76	orbi12d	$⊢ x = seq 1 (+ G) (M) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
78	77	moi2	$⊢ ((seq 1 (+ G) (M) \in V \land \exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))) \land ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))) \to x = seq 1 (+ G) (M)$
79	7 78	mpanl1	$⊢ (\exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))) \to x = seq 1 (+ G) (M)$
80	79	ancom2s	$⊢ (\exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))) \to x = seq 1 (+ G) (M)$
81	80	expr	$⊢ (\exists^{*} x (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (+ G) (M) = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \to x = seq 1 (+ G) (M))$
82	24 69 81	syl2anc	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \to x = seq 1 (+ G) (M))$
83	69 77	syl5ibrcom	$⊢ φ \to (x = seq 1 (+ G) (M) \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
84	82 83	impbid	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \leftrightarrow x = seq 1 (+ G) (M))$
85	84	adantr	$⊢ (φ \land seq 1 (+ G) (M) \in V) \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \leftrightarrow x = seq 1 (+ G) (M))$
86	85	iota5	$⊢ (φ \land seq 1 (+ G) (M) \in V) \to (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))) = seq 1 (+ G) (M)$
87	7 86	mpan2	$⊢ φ \to (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))) = seq 1 (+ G) (M)$
88	6 87	syl5eq	$⊢ φ \to \sum_{k \in A} B = seq 1 (+ G) (M)$

Metamath Proof Explorer

Theorem fsum

Proof