fsumrev

Description: Reversal of a finite sum. (Contributed by NM, 26-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsumrev.1	$⊢ φ \to K \in ℤ$
	fsumrev.2	$⊢ φ \to M \in ℤ$
	fsumrev.3	$⊢ φ \to N \in ℤ$
	fsumrev.4	$⊢ (φ \land j \in (M \dots N)) \to A \in ℂ$
	fsumrev.5	$⊢ j = K - k \to A = B$
Assertion	fsumrev	$⊢ φ \to \sum_{j = M}^{N} A = \sum_{k = K - N}^{K - M} B$

Proof

Step	Hyp	Ref	Expression
1		fsumrev.1	$⊢ φ \to K \in ℤ$
2		fsumrev.2	$⊢ φ \to M \in ℤ$
3		fsumrev.3	$⊢ φ \to N \in ℤ$
4		fsumrev.4	$⊢ (φ \land j \in (M \dots N)) \to A \in ℂ$
5		fsumrev.5	$⊢ j = K - k \to A = B$
6		fzfid	$⊢ φ \to (K - N \dots K - M) \in Fin$
7		eqid	$⊢ (j \in (K - N \dots K - M) ⟼ K - j) = (j \in (K - N \dots K - M) ⟼ K - j)$
8		ovexd	$⊢ (φ \land j \in (K - N \dots K - M)) \to K - j \in V$
9		ovexd	$⊢ (φ \land k \in (M \dots N)) \to K - k \in V$
10		simprr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to k = K - j$
11		simprl	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j \in (K - N \dots K - M)$
12	2	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to M \in ℤ$
13	3	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to N \in ℤ$
14	1	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K \in ℤ$
15		elfzelz	$⊢ j \in (K - N \dots K - M) \to j \in ℤ$
16	11 15	syl	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j \in ℤ$
17		fzrev	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land j \in ℤ)) \to (j \in (K - N \dots K - M) \leftrightarrow K - j \in (M \dots N))$
18	12 13 14 16 17	syl22anc	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to (j \in (K - N \dots K - M) \leftrightarrow K - j \in (M \dots N))$
19	11 18	mpbid	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - j \in (M \dots N)$
20	10 19	eqeltrd	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to k \in (M \dots N)$
21	10	oveq2d	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - k = K - (K - j)$
22		zcn	$⊢ K \in ℤ \to K \in ℂ$
23		zcn	$⊢ j \in ℤ \to j \in ℂ$
24		nncan	$⊢ (K \in ℂ \land j \in ℂ) \to K - (K - j) = j$
25	22 23 24	syl2an	$⊢ (K \in ℤ \land j \in ℤ) \to K - (K - j) = j$
26	1 16 25	syl2an2r	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - (K - j) = j$
27	21 26	eqtr2d	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j = K - k$
28	20 27	jca	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to (k \in (M \dots N) \land j = K - k)$
29		simprr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to j = K - k$
30		simprl	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k \in (M \dots N)$
31	2	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to M \in ℤ$
32	3	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to N \in ℤ$
33	1	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K \in ℤ$
34		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
35	30 34	syl	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k \in ℤ$
36		fzrev2	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land k \in ℤ)) \to (k \in (M \dots N) \leftrightarrow K - k \in (K - N \dots K - M))$
37	31 32 33 35 36	syl22anc	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to (k \in (M \dots N) \leftrightarrow K - k \in (K - N \dots K - M))$
38	30 37	mpbid	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - k \in (K - N \dots K - M)$
39	29 38	eqeltrd	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to j \in (K - N \dots K - M)$
40	29	oveq2d	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - j = K - (K - k)$
41		zcn	$⊢ k \in ℤ \to k \in ℂ$
42		nncan	$⊢ (K \in ℂ \land k \in ℂ) \to K - (K - k) = k$
43	22 41 42	syl2an	$⊢ (K \in ℤ \land k \in ℤ) \to K - (K - k) = k$
44	1 35 43	syl2an2r	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - (K - k) = k$
45	40 44	eqtr2d	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k = K - j$
46	39 45	jca	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to (j \in (K - N \dots K - M) \land k = K - j)$
47	28 46	impbida	$⊢ φ \to ((j \in (K - N \dots K - M) \land k = K - j) \leftrightarrow (k \in (M \dots N) \land j = K - k))$
48	7 8 9 47	f1od	$⊢ φ \to (j \in (K - N \dots K - M) ⟼ K - j) : (K - N \dots K - M) \underset{1-1 onto}{⟶} (M \dots N)$
49		oveq2	$⊢ j = k \to K - j = K - k$
50		ovex	$⊢ K - k \in V$
51	49 7 50	fvmpt	$⊢ k \in (K - N \dots K - M) \to (j \in (K - N \dots K - M) ⟼ K - j) (k) = K - k$
52	51	adantl	$⊢ (φ \land k \in (K - N \dots K - M)) \to (j \in (K - N \dots K - M) ⟼ K - j) (k) = K - k$
53	5 6 48 52 4	fsumf1o	$⊢ φ \to \sum_{j = M}^{N} A = \sum_{k = K - N}^{K - M} B$

Metamath Proof Explorer

Theorem fsumrev

Proof