Theorem fsumrev2

Description: Reversal of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Hypotheses	fsumrev2.1	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
	fsumrev2.2	$$⊢j=M+N-k\to A=B$$
Assertion	fsumrev2	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumrev2.1	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
2		fsumrev2.2	$$⊢j=M+N-k\to A=B$$
3		sum0	$$⊢\sum _{j\in \varnothing }A=0$$
4		sum0	$$⊢\sum _{k\in \varnothing }B=0$$
5	3 4	eqtr4i	$$⊢\sum _{j\in \varnothing }A=\sum _{k\in \varnothing }B$$
6		sumeq1	$$⊢\left(M\dots N\right)=\varnothing \to \sum _{j=M}^{N}A=\sum _{j\in \varnothing }A$$
7		sumeq1	$$⊢\left(M\dots N\right)=\varnothing \to \sum _{k=M}^{N}B=\sum _{k\in \varnothing }B$$
8	5 6 7	3eqtr4a	$$⊢\left(M\dots N\right)=\varnothing \to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$
9	8	adantl	$$⊢\left(\phi \wedge \left(M\dots N\right)=\varnothing \right)\to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$
10		fzn0	$$⊢\left(M\dots N\right)\ne \varnothing \leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$
11		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
12	11	adantl	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to M\in \mathbb{Z}$$
13		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
14	13	adantl	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to N\in \mathbb{Z}$$
15	12 14	zaddcld	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to M+N\in \mathbb{Z}$$
16	1	adantlr	$$⊢\left(\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
17	15 12 14 16 2	fsumrev	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to \sum _{j=M}^{N}A=\sum _{k=M+N-N}^{M+N-M}B$$
18	12	zcnd	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to M\in ℂ$$
19	14	zcnd	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to N\in ℂ$$
20	18 19	pncand	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to M+N-N=M$$
21	18 19	pncan2d	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to M+N-M=N$$
22	20 21	oveq12d	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to \left(M+N-N\dots M+N-M\right)=\left(M\dots N\right)$$
23	22	sumeq1d	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to \sum _{k=M+N-N}^{M+N-M}B=\sum _{k=M}^{N}B$$
24	17 23	eqtrd	$$⊢\left(\phi \wedge N\in {\mathbb{Z}}_{\ge M}\right)\to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$
25	10 24	sylan2b	$$⊢\left(\phi \wedge \left(M\dots N\right)\ne \varnothing \right)\to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$
26	9 25	pm2.61dane	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M}^{N}B$$