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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumdvds.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fsumdvds.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
	fsumdvds.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ∥ 𝐵 )
Assertion	fsumdvds	⊢ ( 𝜑 → 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsumdvds.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fsumdvds.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		fsumdvds.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
4		fsumdvds.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ∥ 𝐵 )
5		0z	⊢ 0 ∈ ℤ
6		dvds0	⊢ ( 0 ∈ ℤ → 0 ∥ 0 )
7	5 6	mp1i	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 0 ∥ 0 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
9		simplr	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑁 = 0 )
10	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ∥ 𝐵 )
11	9 10	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 0 ∥ 𝐵 )
12	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
13		0dvds	⊢ ( 𝐵 ∈ ℤ → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
14	12 13	syl	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
15	11 14	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 = 0 )
16	15	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 0 )
17	1	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐴 ∈ Fin )
18	17	olcd	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝐴 ⊆ ( ℤ_≥ ‘ 0 ) ∨ 𝐴 ∈ Fin ) )
19		sumz	⊢ ( ( 𝐴 ⊆ ( ℤ_≥ ‘ 0 ) ∨ 𝐴 ∈ Fin ) → Σ 𝑘 ∈ 𝐴 0 = 0 )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → Σ 𝑘 ∈ 𝐴 0 = 0 )
21	16 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → Σ 𝑘 ∈ 𝐴 𝐵 = 0 )
22	7 8 21	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )
23	1	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ Fin )
24	2	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℤ )
25	24	zcnd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℂ )
26	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
27	26	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → 𝑁 ≠ 0 )
29	23 25 27 28	fsumdivc	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → ( Σ 𝑘 ∈ 𝐴 𝐵 / 𝑁 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 / 𝑁 ) )
30	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ∥ 𝐵 )
31	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ∈ ℤ )
32		simplr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑁 ≠ 0 )
33		dvdsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∥ 𝐵 ↔ ( 𝐵 / 𝑁 ) ∈ ℤ ) )
34	31 32 26 33	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑁 ∥ 𝐵 ↔ ( 𝐵 / 𝑁 ) ∈ ℤ ) )
35	30 34	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 / 𝑁 ) ∈ ℤ )
36	23 35	fsumzcl	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 / 𝑁 ) ∈ ℤ )
37	29 36	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → ( Σ 𝑘 ∈ 𝐴 𝐵 / 𝑁 ) ∈ ℤ )
38	1 3	fsumzcl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
40		dvdsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 / 𝑁 ) ∈ ℤ ) )
41	24 28 39 40	syl3anc	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → ( 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 / 𝑁 ) ∈ ℤ ) )
42	37 41	mpbird	⊢ ( ( 𝜑 ∧ 𝑁 ≠ 0 ) → 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )
43	22 42	pm2.61dane	⊢ ( 𝜑 → 𝑁 ∥ Σ 𝑘 ∈ 𝐴 𝐵 )

Metamath Proof Explorer

Theorem fsumdvds

Proof