sumeven

Description: If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021)

	Ref	Expression
Hypotheses	sumeven.a	$⊢ φ \to A \in Fin$
	sumeven.b	$⊢ (φ \land k \in A) \to B \in ℤ$
	sumeven.e	$⊢ (φ \land k \in A) \to 2 ∥ B$
Assertion	sumeven	$⊢ φ \to 2 ∥ \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		sumeven.a	$⊢ φ \to A \in Fin$
2		sumeven.b	$⊢ (φ \land k \in A) \to B \in ℤ$
3		sumeven.e	$⊢ (φ \land k \in A) \to 2 ∥ B$
4		sumeq1	$⊢ x = \emptyset \to \sum_{k \in x} B = \sum_{k \in \emptyset} B$
5	4	breq2d	$⊢ x = \emptyset \to (2 ∥ \sum_{k \in x} B \leftrightarrow 2 ∥ \sum_{k \in \emptyset} B)$
6		sumeq1	$⊢ x = y \to \sum_{k \in x} B = \sum_{k \in y} B$
7	6	breq2d	$⊢ x = y \to (2 ∥ \sum_{k \in x} B \leftrightarrow 2 ∥ \sum_{k \in y} B)$
8		sumeq1	$⊢ x = y \cup \{z\} \to \sum_{k \in x} B = \sum_{k \in y \cup \{z\}} B$
9	8	breq2d	$⊢ x = y \cup \{z\} \to (2 ∥ \sum_{k \in x} B \leftrightarrow 2 ∥ \sum_{k \in y \cup \{z\}} B)$
10		sumeq1	$⊢ x = A \to \sum_{k \in x} B = \sum_{k \in A} B$
11	10	breq2d	$⊢ x = A \to (2 ∥ \sum_{k \in x} B \leftrightarrow 2 ∥ \sum_{k \in A} B)$
12		z0even	$⊢ 2 ∥ 0$
13		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
14	12 13	breqtrri	$⊢ 2 ∥ \sum_{k \in \emptyset} B$
15	14	a1i	$⊢ φ \to 2 ∥ \sum_{k \in \emptyset} B$
16		2z	$⊢ 2 \in ℤ$
17	16	a1i	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to 2 \in ℤ$
18		ssfi	$⊢ (A \in Fin \land y \subseteq A) \to y \in Fin$
19	18	expcom	$⊢ y \subseteq A \to (A \in Fin \to y \in Fin)$
20	19	adantr	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to (A \in Fin \to y \in Fin)$
21	1 20	mpan9	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to y \in Fin$
22		simpll	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to φ$
23		ssel	$⊢ y \subseteq A \to (k \in y \to k \in A)$
24	23	adantr	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to (k \in y \to k \in A)$
25	24	adantl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (k \in y \to k \in A)$
26	25	imp	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to k \in A$
27	22 26 2	syl2anc	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to B \in ℤ$
28	21 27	fsumzcl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \sum_{k \in y} B \in ℤ$
29		eldifi	$⊢ z \in (A ∖ y) \to z \in A$
30	29	adantl	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to z \in A$
31	30	adantl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in A$
32	2	adantlr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in A) \to B \in ℤ$
33	32	ralrimiva	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \forall k \in A B \in ℤ$
34		rspcsbela	$⊢ (z \in A \land \forall k \in A B \in ℤ) \to ⦋ z / k ⦌ B \in ℤ$
35	31 33 34	syl2anc	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to ⦋ z / k ⦌ B \in ℤ$
36	17 28 35	3jca	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (2 \in ℤ \land \sum_{k \in y} B \in ℤ \land ⦋ z / k ⦌ B \in ℤ)$
37	36	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land 2 ∥ \sum_{k \in y} B) \to (2 \in ℤ \land \sum_{k \in y} B \in ℤ \land ⦋ z / k ⦌ B \in ℤ)$
38	3	ralrimiva	$⊢ φ \to \forall k \in A 2 ∥ B$
39		nfcv	$⊢ \underline{Ⅎ} k 2$
40		nfcv	$⊢ \underline{Ⅎ} k ∥$
41		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
42	39 40 41	nfbr	$⊢ Ⅎ k 2 ∥ ⦋ z / k ⦌ B$
43		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
44	43	breq2d	$⊢ k = z \to (2 ∥ B \leftrightarrow 2 ∥ ⦋ z / k ⦌ B)$
45	42 44	rspc	$⊢ z \in A \to (\forall k \in A 2 ∥ B \to 2 ∥ ⦋ z / k ⦌ B)$
46	29 38 45	syl2imc	$⊢ φ \to (z \in (A ∖ y) \to 2 ∥ ⦋ z / k ⦌ B)$
47	46	a1d	$⊢ φ \to (y \subseteq A \to (z \in (A ∖ y) \to 2 ∥ ⦋ z / k ⦌ B))$
48	47	imp32	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to 2 ∥ ⦋ z / k ⦌ B$
49	48	anim1ci	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land 2 ∥ \sum_{k \in y} B) \to (2 ∥ \sum_{k \in y} B \land 2 ∥ ⦋ z / k ⦌ B)$
50		dvds2add	$⊢ (2 \in ℤ \land \sum_{k \in y} B \in ℤ \land ⦋ z / k ⦌ B \in ℤ) \to ((2 ∥ \sum_{k \in y} B \land 2 ∥ ⦋ z / k ⦌ B) \to 2 ∥ (\sum_{k \in y} B + ⦋ z / k ⦌ B))$
51	37 49 50	sylc	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land 2 ∥ \sum_{k \in y} B) \to 2 ∥ (\sum_{k \in y} B + ⦋ z / k ⦌ B)$
52		vex	$⊢ z \in V$
53	52	a1i	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in V$
54		eldif	$⊢ z \in (A ∖ y) \leftrightarrow (z \in A \land \neg z \in y)$
55		df-nel	$⊢ z \notin y \leftrightarrow \neg z \in y$
56	55	biimpri	$⊢ \neg z \in y \to z \notin y$
57	54 56	simplbiim	$⊢ z \in (A ∖ y) \to z \notin y$
58	57	adantl	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to z \notin y$
59	58	adantl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \notin y$
60		simpll	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in (y \cup \{z\})) \to φ$
61		elun	$⊢ k \in (y \cup \{z\}) \leftrightarrow (k \in y \lor k \in \{z\})$
62	24	com12	$⊢ k \in y \to ((y \subseteq A \land z \in (A ∖ y)) \to k \in A)$
63		elsni	$⊢ k \in \{z\} \to k = z$
64		eleq1w	$⊢ k = z \to (k \in A \leftrightarrow z \in A)$
65	30 64	syl5ibr	$⊢ k = z \to ((y \subseteq A \land z \in (A ∖ y)) \to k \in A)$
66	63 65	syl	$⊢ k \in \{z\} \to ((y \subseteq A \land z \in (A ∖ y)) \to k \in A)$
67	62 66	jaoi	$⊢ (k \in y \lor k \in \{z\}) \to ((y \subseteq A \land z \in (A ∖ y)) \to k \in A)$
68	67	com12	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to ((k \in y \lor k \in \{z\}) \to k \in A)$
69	61 68	syl5bi	$⊢ (y \subseteq A \land z \in (A ∖ y)) \to (k \in (y \cup \{z\}) \to k \in A)$
70	69	adantl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (k \in (y \cup \{z\}) \to k \in A)$
71	70	imp	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in (y \cup \{z\})) \to k \in A$
72	60 71 2	syl2anc	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in (y \cup \{z\})) \to B \in ℤ$
73	72	ralrimiva	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \forall k \in (y \cup \{z\}) B \in ℤ$
74		fsumsplitsnun	$⊢ (y \in Fin \land (z \in V \land z \notin y) \land \forall k \in (y \cup \{z\}) B \in ℤ) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
75	21 53 59 73 74	syl121anc	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
76	75	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land 2 ∥ \sum_{k \in y} B) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
77	51 76	breqtrrd	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land 2 ∥ \sum_{k \in y} B) \to 2 ∥ \sum_{k \in y \cup \{z\}} B$
78	77	ex	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (2 ∥ \sum_{k \in y} B \to 2 ∥ \sum_{k \in y \cup \{z\}} B)$
79	5 7 9 11 15 78 1	findcard2d	$⊢ φ \to 2 ∥ \sum_{k \in A} B$

Metamath Proof Explorer

Theorem sumeven

Proof