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

Metamath Proof Explorer

Theorem fsumrev

Proof