Theorem geoserg

Description: The value of the finite geometric series A ^ M + A ^ ( M + 1 ) + ... + A ^ ( N - 1 ) . (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	geoserg.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	geoserg.2	⊢ ( 𝜑 → 𝐴 ≠ 1 )
	geoserg.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	geoserg.4	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
Assertion	geoserg	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		geoserg.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		geoserg.2	⊢ ( 𝜑 → 𝐴 ≠ 1 )
3		geoserg.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4		geoserg.4	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5		fzofi	⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
6	5	a1i	⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
7		ax-1cn	⊢ 1 ∈ ℂ
8		subcl	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
9	7 1 8	sylancr	⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
10	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
11		elfzouz	⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
12		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
13	3 11 12	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
14	10 13	expcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
15	6 9 14	fsummulc1	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) )
16	7	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 1 ∈ ℂ )
17	14 16 10	subdid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = ( ( ( 𝐴 ↑ 𝑘 ) · 1 ) − ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
18	14	mulid1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · 1 ) = ( 𝐴 ↑ 𝑘 ) )
19	10 13	expp1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
20	19	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
21	18 20	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐴 ↑ 𝑘 ) · 1 ) − ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
22	17 21	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
23	22	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
24		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
25		oveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
26		oveq2	⊢ ( 𝑗 = 𝑀 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑀 ) )
27		oveq2	⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
28	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
29		elfzuz	⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
30		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
31	3 29 30	syl2an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 ∈ ℕ0 )
32	28 31	expcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
33	24 25 26 27 4 32	telfsumo	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) − ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) )
34	15 23 33	3eqtrrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) )
35	1 3	expcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
36		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
37	3 4 36	syl2anc	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
38	1 37	expcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
39	35 38	subcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
40	6 14	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
41	2	necomd	⊢ ( 𝜑 → 1 ≠ 𝐴 )
42		subeq0	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
43	7 1 42	sylancr	⊢ ( 𝜑 → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
44	43	necon3bid	⊢ ( 𝜑 → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
45	41 44	mpbird	⊢ ( 𝜑 → ( 1 − 𝐴 ) ≠ 0 )
46	39 40 9 45	divmul3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) ↔ ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) · ( 1 − 𝐴 ) ) ) )
47	34 46	mpbird	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) )
48	47	eqcomd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )