fsumdvds

Description: If every term in a sum is divisible by N , then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Hypotheses	fsumdvds.1	$⊢ φ \to A \in Fin$
	fsumdvds.2	$⊢ φ \to N \in ℤ$
	fsumdvds.3	$⊢ (φ \land k \in A) \to B \in ℤ$
	fsumdvds.4	$⊢ (φ \land k \in A) \to N ∥ B$
Assertion	fsumdvds	$⊢ φ \to N ∥ \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		fsumdvds.1	$⊢ φ \to A \in Fin$
2		fsumdvds.2	$⊢ φ \to N \in ℤ$
3		fsumdvds.3	$⊢ (φ \land k \in A) \to B \in ℤ$
4		fsumdvds.4	$⊢ (φ \land k \in A) \to N ∥ B$
5		0z	$⊢ 0 \in ℤ$
6		dvds0	$⊢ 0 \in ℤ \to 0 ∥ 0$
7	5 6	mp1i	$⊢ (φ \land N = 0) \to 0 ∥ 0$
8		simpr	$⊢ (φ \land N = 0) \to N = 0$
9		simplr	$⊢ ((φ \land N = 0) \land k \in A) \to N = 0$
10	4	adantlr	$⊢ ((φ \land N = 0) \land k \in A) \to N ∥ B$
11	9 10	eqbrtrrd	$⊢ ((φ \land N = 0) \land k \in A) \to 0 ∥ B$
12	3	adantlr	$⊢ ((φ \land N = 0) \land k \in A) \to B \in ℤ$
13		0dvds	$⊢ B \in ℤ \to (0 ∥ B \leftrightarrow B = 0)$
14	12 13	syl	$⊢ ((φ \land N = 0) \land k \in A) \to (0 ∥ B \leftrightarrow B = 0)$
15	11 14	mpbid	$⊢ ((φ \land N = 0) \land k \in A) \to B = 0$
16	15	sumeq2dv	$⊢ (φ \land N = 0) \to \sum_{k \in A} B = \sum_{k \in A} 0$
17	1	adantr	$⊢ (φ \land N = 0) \to A \in Fin$
18	17	olcd	$⊢ (φ \land N = 0) \to (A \subseteq ℤ_{\geq 0} \lor A \in Fin)$
19		sumz	$⊢ (A \subseteq ℤ_{\geq 0} \lor A \in Fin) \to \sum_{k \in A} 0 = 0$
20	18 19	syl	$⊢ (φ \land N = 0) \to \sum_{k \in A} 0 = 0$
21	16 20	eqtrd	$⊢ (φ \land N = 0) \to \sum_{k \in A} B = 0$
22	7 8 21	3brtr4d	$⊢ (φ \land N = 0) \to N ∥ \sum_{k \in A} B$
23	1	adantr	$⊢ (φ \land N \neq 0) \to A \in Fin$
24	2	adantr	$⊢ (φ \land N \neq 0) \to N \in ℤ$
25	24	zcnd	$⊢ (φ \land N \neq 0) \to N \in ℂ$
26	3	adantlr	$⊢ ((φ \land N \neq 0) \land k \in A) \to B \in ℤ$
27	26	zcnd	$⊢ ((φ \land N \neq 0) \land k \in A) \to B \in ℂ$
28		simpr	$⊢ (φ \land N \neq 0) \to N \neq 0$
29	23 25 27 28	fsumdivc	$⊢ (φ \land N \neq 0) \to \frac{\sum_{k \in A} B}{N} = \sum_{k \in A} (\frac{B}{N})$
30	4	adantlr	$⊢ ((φ \land N \neq 0) \land k \in A) \to N ∥ B$
31	24	adantr	$⊢ ((φ \land N \neq 0) \land k \in A) \to N \in ℤ$
32		simplr	$⊢ ((φ \land N \neq 0) \land k \in A) \to N \neq 0$
33		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land B \in ℤ) \to (N ∥ B \leftrightarrow \frac{B}{N} \in ℤ)$
34	31 32 26 33	syl3anc	$⊢ ((φ \land N \neq 0) \land k \in A) \to (N ∥ B \leftrightarrow \frac{B}{N} \in ℤ)$
35	30 34	mpbid	$⊢ ((φ \land N \neq 0) \land k \in A) \to \frac{B}{N} \in ℤ$
36	23 35	fsumzcl	$⊢ (φ \land N \neq 0) \to \sum_{k \in A} (\frac{B}{N}) \in ℤ$
37	29 36	eqeltrd	$⊢ (φ \land N \neq 0) \to \frac{\sum_{k \in A} B}{N} \in ℤ$
38	1 3	fsumzcl	$⊢ φ \to \sum_{k \in A} B \in ℤ$
39	38	adantr	$⊢ (φ \land N \neq 0) \to \sum_{k \in A} B \in ℤ$
40		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land \sum_{k \in A} B \in ℤ) \to (N ∥ \sum_{k \in A} B \leftrightarrow \frac{\sum_{k \in A} B}{N} \in ℤ)$
41	24 28 39 40	syl3anc	$⊢ (φ \land N \neq 0) \to (N ∥ \sum_{k \in A} B \leftrightarrow \frac{\sum_{k \in A} B}{N} \in ℤ)$
42	37 41	mpbird	$⊢ (φ \land N \neq 0) \to N ∥ \sum_{k \in A} B$
43	22 42	pm2.61dane	$⊢ φ \to N ∥ \sum_{k \in A} B$

Metamath Proof Explorer

Theorem fsumdvds

Proof