Theorem fsumm1

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	fsumm1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fsumm1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fsumm1.3	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
Assertion	fsumm1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fsumm1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fsumm1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
3		fsumm1.3	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
4		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
5	1 4	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6		fzsn	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
7	5 6	syl	⊢ ( 𝜑 → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
8	7	ineq2d	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( 𝑁 ... 𝑁 ) ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) )
9	5	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10	9	ltm1d	⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
11		fzdisj	⊢ ( ( 𝑁 − 1 ) < 𝑁 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( 𝑁 ... 𝑁 ) ) = ∅ )
12	10 11	syl	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( 𝑁 ... 𝑁 ) ) = ∅ )
13	8 12	eqtr3d	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ { 𝑁 } ) = ∅ )
14		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
15	1 14	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
16		peano2zm	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
17	15 16	syl	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
18	15	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
19		ax-1cn	⊢ 1 ∈ ℂ
20		npcan	⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
21	18 19 20	sylancl	⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
22	21	fveq2d	⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝑀 ) )
23	1 22	eleqtrrd	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) )
24		eluzp1m1	⊢ ( ( ( 𝑀 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
25	17 23 24	syl2anc	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
26		fzsuc2	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { ( ( 𝑁 − 1 ) + 1 ) } ) )
27	15 25 26	syl2anc	⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { ( ( 𝑁 − 1 ) + 1 ) } ) )
28	5	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
29		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
30	28 19 29	sylancl	⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
31	30	oveq2d	⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
32	27 31	eqtr3d	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { ( ( 𝑁 − 1 ) + 1 ) } ) = ( 𝑀 ... 𝑁 ) )
33	30	sneqd	⊢ ( 𝜑 → { ( ( 𝑁 − 1 ) + 1 ) } = { 𝑁 } )
34	33	uneq2d	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { ( ( 𝑁 − 1 ) + 1 ) } ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
35	32 34	eqtr3d	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
36		fzfid	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
37	13 35 36 2	fsumsplit	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + Σ 𝑘 ∈ { 𝑁 } 𝐴 ) )
38	3	eleq1d	⊢ ( 𝑘 = 𝑁 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
39	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
40		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
41	1 40	syl	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
42	38 39 41	rspcdva	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
43	3	sumsn	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑁 } 𝐴 = 𝐵 )
44	1 42 43	syl2anc	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑁 } 𝐴 = 𝐵 )
45	44	oveq2d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + Σ 𝑘 ∈ { 𝑁 } 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )
46	37 45	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )