zsum

Description: Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019)

	Ref	Expression
Hypotheses	zsum.1	$⊢ Z = ℤ_{\geq M}$
	zsum.2	$⊢ φ \to M \in ℤ$
	zsum.3	$⊢ φ \to A \subseteq Z$
	zsum.4	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 0)$
	zsum.5	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	zsum	$⊢ φ \to \sum_{k \in A} B = ⇝ (seq M (+ F))$

Proof

Step	Hyp	Ref	Expression
1		zsum.1	$⊢ Z = ℤ_{\geq M}$
2		zsum.2	$⊢ φ \to M \in ℤ$
3		zsum.3	$⊢ φ \to A \subseteq Z$
4		zsum.4	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 0)$
5		zsum.5	$⊢ (φ \land k \in A) \to B \in ℂ$
6		eleq1w	$⊢ n = i \to (n \in A \leftrightarrow i \in A)$
7		csbeq1	$⊢ n = i \to ⦋ n / k ⦌ B = ⦋ i / k ⦌ B$
8	6 7	ifbieq1d	$⊢ n = i \to if (n \in A, ⦋ n / k ⦌ B, 0) = if (i \in A, ⦋ i / k ⦌ B, 0)$
9	8	cbvmptv	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) = (i \in ℤ ⟼ if (i \in A, ⦋ i / k ⦌ B, 0))$
10		simpll	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to φ$
11	5	ralrimiva	$⊢ φ \to \forall k \in A B \in ℂ$
12		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ B$
13	12	nfel1	$⊢ Ⅎ k ⦋ i / k ⦌ B \in ℂ$
14		csbeq1a	$⊢ k = i \to B = ⦋ i / k ⦌ B$
15	14	eleq1d	$⊢ k = i \to (B \in ℂ \leftrightarrow ⦋ i / k ⦌ B \in ℂ)$
16	13 15	rspc	$⊢ i \in A \to (\forall k \in A B \in ℂ \to ⦋ i / k ⦌ B \in ℂ)$
17	11 16	syl5	$⊢ i \in A \to (φ \to ⦋ i / k ⦌ B \in ℂ)$
18	10 17	mpan9	$⊢ (((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \land i \in A) \to ⦋ i / k ⦌ B \in ℂ$
19		simplr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to m \in ℤ$
20	2	ad2antrr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to M \in ℤ$
21		simpr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to A \subseteq ℤ_{\geq m}$
22	3 1	sseqtrdi	$⊢ φ \to A \subseteq ℤ_{\geq M}$
23	22	ad2antrr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to A \subseteq ℤ_{\geq M}$
24	9 18 19 20 21 23	sumrb	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq 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))) ⇝ x)$
25	24	biimpd	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to (seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
26	25	expimpd	$⊢ (φ \land m \in ℤ) \to ((A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
27	26	rexlimdva	$⊢ φ \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
28	3	ad2antrr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \subseteq Z$
29		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
30	1 29	eqsstri	$⊢ Z \subseteq ℤ$
31		zssre	$⊢ ℤ \subseteq ℝ$
32	30 31	sstri	$⊢ Z \subseteq ℝ$
33		ltso	$⊢ < Or ℝ$
34		soss	$⊢ Z \subseteq ℝ \to (< Or ℝ \to < Or Z)$
35	32 33 34	mp2	$⊢ < Or Z$
36		soss	$⊢ A \subseteq Z \to (< Or Z \to < Or A)$
37	28 35 36	mpisyl	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to < Or A$
38		fzfi	$⊢ (1 \dots m) \in Fin$
39		ovex	$⊢ (1 \dots m) \in V$
40	39	f1oen	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to (1 \dots m) \approx A$
41	40	adantl	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (1 \dots m) \approx A$
42	41	ensymd	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \approx (1 \dots m)$
43		enfii	$⊢ ((1 \dots m) \in Fin \land A \approx (1 \dots m)) \to A \in Fin$
44	38 42 43	sylancr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \in Fin$
45		fz1iso	$⊢ (< Or A \land A \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
46	37 44 45	syl2anc	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
47		simpll	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to φ$
48	47 17	mpan9	$⊢ (((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \land i \in A) \to ⦋ i / k ⦌ B \in ℂ$
49		fveq2	$⊢ n = j \to f (n) = f (j)$
50	49	csbeq1d	$⊢ n = j \to ⦋ f (n) / k ⦌ B = ⦋ f (j) / k ⦌ B$
51		csbcow	$⊢ ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B = ⦋ f (j) / k ⦌ B$
52	50 51	eqtr4di	$⊢ n = j \to ⦋ f (n) / k ⦌ B = ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B$
53	52	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (j \in ℕ ⟼ ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B)$
54		eqid	$⊢ (j \in ℕ ⟼ ⦋ g (j) / i ⦌ ⦋ i / k ⦌ B) = (j \in ℕ ⟼ ⦋ g (j) / i ⦌ ⦋ i / k ⦌ B)$
55		simplr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to m \in ℕ$
56	2	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to M \in ℤ$
57	22	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to A \subseteq ℤ_{\geq M}$
58		simprl	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to f : (1 \dots m) \underset{1-1 onto}{⟶} A$
59		simprr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to g {Isom}_{<, <} ((1 \dots \|A\|), A)$
60	9 48 53 54 55 56 57 58 59	summolem2a	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
61	60	expr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
62	61	exlimdv	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (\exists g g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
63	46 62	mpd	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
64		breq2	$⊢ x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (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 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
65	63 64	syl5ibrcom	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
66	65	expimpd	$⊢ (φ \land m \in ℕ) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
67	66	exlimdv	$⊢ (φ \land m \in ℕ) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (+ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
68	67	rexlimdva	$⊢ φ \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)) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
69	27 68	jaod	$⊢ φ \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 seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
70	2	adantr	$⊢ (φ \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to M \in ℤ$
71	22	adantr	$⊢ (φ \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to A \subseteq ℤ_{\geq M}$
72		simpr	$⊢ (φ \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x$
73		fveq2	$⊢ m = M \to ℤ_{\geq m} = ℤ_{\geq M}$
74	73	sseq2d	$⊢ m = M \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq M})$
75		seqeq1	$⊢ m = M \to seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) = seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)))$
76	75	breq1d	$⊢ m = 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))) ⇝ x)$
77	74 76	anbi12d	$⊢ m = 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))) ⇝ x))$
78	77	rspcev	$⊢ (M \in ℤ \land (A \subseteq ℤ_{\geq M} \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)) \to \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
79	70 71 72 78	syl12anc	$⊢ (φ \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \to \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land seq m (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
80	79	orcd	$⊢ (φ \land seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x) \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)))$
81	80	ex	$⊢ φ \to (seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x \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))))$
82	69 81	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 seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x)$
83		simpr	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in ℤ_{\geq M}$
84	29 83	sseldi	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in ℤ$
85	83 1	eleqtrrdi	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in Z$
86	4	ralrimiva	$⊢ φ \to \forall k \in Z F (k) = if (k \in A, B, 0)$
87	86	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to \forall k \in Z F (k) = if (k \in A, B, 0)$
88		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ if (k \in A, B, 0)$
89	88	nfeq2	$⊢ Ⅎ k F (j) = ⦋ j / k ⦌ if (k \in A, B, 0)$
90		fveq2	$⊢ k = j \to F (k) = F (j)$
91		csbeq1a	$⊢ k = j \to if (k \in A, B, 0) = ⦋ j / k ⦌ if (k \in A, B, 0)$
92	90 91	eqeq12d	$⊢ k = j \to (F (k) = if (k \in A, B, 0) \leftrightarrow F (j) = ⦋ j / k ⦌ if (k \in A, B, 0))$
93	89 92	rspc	$⊢ j \in Z \to (\forall k \in Z F (k) = if (k \in A, B, 0) \to F (j) = ⦋ j / k ⦌ if (k \in A, B, 0))$
94	85 87 93	sylc	$⊢ (φ \land j \in ℤ_{\geq M}) \to F (j) = ⦋ j / k ⦌ if (k \in A, B, 0)$
95		fvex	$⊢ F (j) \in V$
96	94 95	eqeltrrdi	$⊢ (φ \land j \in ℤ_{\geq M}) \to ⦋ j / k ⦌ if (k \in A, B, 0) \in V$
97		nfcv	$⊢ \underline{Ⅎ} n if (k \in A, B, 0)$
98		nfv	$⊢ Ⅎ k n \in A$
99		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
100		nfcv	$⊢ \underline{Ⅎ} k 0$
101	98 99 100	nfif	$⊢ \underline{Ⅎ} k if (n \in A, ⦋ n / k ⦌ B, 0)$
102		eleq1w	$⊢ k = n \to (k \in A \leftrightarrow n \in A)$
103		csbeq1a	$⊢ k = n \to B = ⦋ n / k ⦌ B$
104	102 103	ifbieq1d	$⊢ k = n \to if (k \in A, B, 0) = if (n \in A, ⦋ n / k ⦌ B, 0)$
105	97 101 104	cbvmpt	$⊢ (k \in ℤ ⟼ if (k \in A, B, 0)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))$
106	105	eqcomi	$⊢ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) = (k \in ℤ ⟼ if (k \in A, B, 0))$
107	106	fvmpts	$⊢ (j \in ℤ \land ⦋ j / k ⦌ if (k \in A, B, 0) \in V) \to (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) (j) = ⦋ j / k ⦌ if (k \in A, B, 0)$
108	84 96 107	syl2anc	$⊢ (φ \land j \in ℤ_{\geq M}) \to (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) (j) = ⦋ j / k ⦌ if (k \in A, B, 0)$
109	108 94	eqtr4d	$⊢ (φ \land j \in ℤ_{\geq M}) \to (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0)) (j) = F (j)$
110	2 109	seqfeq	$⊢ φ \to seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) = seq M (+ F)$
111	110	breq1d	$⊢ φ \to (seq M (+ (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))) ⇝ x \leftrightarrow seq M (+ F) ⇝ x)$
112	82 111	bitrd	$⊢ φ \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 seq M (+ F) ⇝ x)$
113	112	iotabidv	$⊢ φ \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)))) = (ι x \| seq M (+ F) ⇝ x)$
114		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))))$
115		df-fv	$⊢ ⇝ (seq M (+ F)) = (ι x \| seq M (+ F) ⇝ x)$
116	113 114 115	3eqtr4g	$⊢ φ \to \sum_{k \in A} B = ⇝ (seq M (+ F))$

Metamath Proof Explorer

Theorem zsum

Proof