Theorem fzosumm1

Description: Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fzosumm1.1	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fzosumm1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
3		fzosumm1.3	⊢ ( 𝑘 = ( 𝑁 − 1 ) → 𝐴 = 𝐵 )
4		fzosumm1.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
6	4 5	syl	⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
7	6	eqcomd	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) = ( 𝑀 ..^ 𝑁 ) )
8	7	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) )
9	8	biimpa	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
10	9 2	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
11	1 10 3	fsumm1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
12	6	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 )
13		eluzelz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
14		fzoval	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑀 ..^ ( 𝑁 − 1 ) ) = ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) )
15	1 13 14	3syl	⊢ ( 𝜑 → ( 𝑀 ..^ ( 𝑁 − 1 ) ) = ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) )
16	15	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 )
17	16	oveq1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
18	11 12 17	3eqtr4d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )