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	$$⊢\phi \to A\in ℂ$$
	geoserg.2	$$⊢\phi \to A\ne 1$$
	geoserg.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	geoserg.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
Assertion	geoserg	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}{A}^k=\frac{A^M-A^N}{1-A}$$

Proof

Step	Hyp	Ref	Expression
1		geoserg.1	$$⊢\phi \to A\in ℂ$$
2		geoserg.2	$$⊢\phi \to A\ne 1$$
3		geoserg.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
4		geoserg.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
5		fzofi	$$⊢\left(M..^N\right)\in \mathrm{Fin}$$
6	5	a1i	$$⊢\phi \to \left(M..^N\right)\in \mathrm{Fin}$$
7		ax-1cn	$$⊢1\in ℂ$$
8		subcl	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to 1-A\in ℂ$$
9	7 1 8	sylancr	$$⊢\phi \to 1-A\in ℂ$$
10	1	adantr	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A\in ℂ$$
11		elfzouz	$$⊢k\in \left(M..^N\right)\to k\in {\mathbb{Z}}_{\ge M}$$
12		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
13	3 11 12	syl2an	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to k\in {\mathbb{N}}_0$$
14	10 13	expcld	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^k\in ℂ$$
15	6 9 14	fsummulc1	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}{A}^k\left(1-A\right)=\sum _{k\in \left(M..^N\right)}{A}^k\left(1-A\right)$$
16	7	a1i	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to 1\in ℂ$$
17	14 16 10	subdid	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^k\left(1-A\right)=A^k\cdot 1-A^{k}A$$
18	14	mulid1d	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^k\cdot 1=A^k$$
19	10 13	expp1d	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^{k+1}=A^{k}A$$
20	19	eqcomd	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^{k}A=A^{k+1}$$
21	18 20	oveq12d	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^k\cdot 1-A^{k}A=A^k-A^{k+1}$$
22	17 21	eqtrd	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A^k\left(1-A\right)=A^k-A^{k+1}$$
23	22	sumeq2dv	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}{A}^k\left(1-A\right)=\sum _{k\in \left(M..^N\right)}\left(A^k-A^{k+1}\right)$$
24		oveq2	$$⊢j=k\to A^j=A^k$$
25		oveq2	$$⊢j=k+1\to A^j=A^{k+1}$$
26		oveq2	$$⊢j=M\to A^j=A^M$$
27		oveq2	$$⊢j=N\to A^j=A^N$$
28	1	adantr	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
29		elfzuz	$$⊢j\in \left(M\dots N\right)\to j\in {\mathbb{Z}}_{\ge M}$$
30		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge j\in {\mathbb{Z}}_{\ge M}\right)\to j\in {\mathbb{N}}_0$$
31	3 29 30	syl2an	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to j\in {\mathbb{N}}_0$$
32	28 31	expcld	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A^j\in ℂ$$
33	24 25 26 27 4 32	telfsumo	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}\left(A^k-A^{k+1}\right)=A^M-A^N$$
34	15 23 33	3eqtrrd	$$⊢\phi \to A^M-A^N=\sum _{k\in \left(M..^N\right)}{A}^k\left(1-A\right)$$
35	1 3	expcld	$$⊢\phi \to A^M\in ℂ$$
36		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\to N\in {\mathbb{N}}_0$$
37	3 4 36	syl2anc	$$⊢\phi \to N\in {\mathbb{N}}_0$$
38	1 37	expcld	$$⊢\phi \to A^N\in ℂ$$
39	35 38	subcld	$$⊢\phi \to A^M-A^N\in ℂ$$
40	6 14	fsumcl	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}{A}^k\in ℂ$$
41	2	necomd	$$⊢\phi \to 1\ne A$$
42		subeq0	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\leftrightarrow 1=A\right)$$
43	7 1 42	sylancr	$$⊢\phi \to \left(1-A=0\leftrightarrow 1=A\right)$$
44	43	necon3bid	$$⊢\phi \to \left(1-A\ne 0\leftrightarrow 1\ne A\right)$$
45	41 44	mpbird	$$⊢\phi \to 1-A\ne 0$$
46	39 40 9 45	divmul3d	$$⊢\phi \to \left(\frac{A^M-A^N}{1-A}=\sum _{k\in \left(M..^N\right)}{A}^k\leftrightarrow A^M-A^N=\sum _{k\in \left(M..^N\right)}{A}^k\left(1-A\right)\right)$$
47	34 46	mpbird	$$⊢\phi \to \frac{A^M-A^N}{1-A}=\sum _{k\in \left(M..^N\right)}{A}^k$$
48	47	eqcomd	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}{A}^k=\frac{A^M-A^N}{1-A}$$