fprodrev

Description: Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		fprodshft.1	$⊢ φ \to K \in ℤ$
2		fprodshft.2	$⊢ φ \to M \in ℤ$
3		fprodshft.3	$⊢ φ \to N \in ℤ$
4		fprodshft.4	$⊢ (φ \land j \in (M \dots N)) \to A \in ℂ$
5		fprodrev.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	1	adantr	$⊢ (φ \land j \in (K - N \dots K - M)) \to K \in ℤ$
9		elfzelz	$⊢ j \in (K - N \dots K - M) \to j \in ℤ$
10	9	adantl	$⊢ (φ \land j \in (K - N \dots K - M)) \to j \in ℤ$
11	8 10	zsubcld	$⊢ (φ \land j \in (K - N \dots K - M)) \to K - j \in ℤ$
12	1	adantr	$⊢ (φ \land k \in (M \dots N)) \to K \in ℤ$
13		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
14	13	adantl	$⊢ (φ \land k \in (M \dots N)) \to k \in ℤ$
15	12 14	zsubcld	$⊢ (φ \land k \in (M \dots N)) \to K - k \in ℤ$
16		simprr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to k = K - j$
17		simprl	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j \in (K - N \dots K - M)$
18	2	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to M \in ℤ$
19	3	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to N \in ℤ$
20	1	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K \in ℤ$
21	9	ad2antrl	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j \in ℤ$
22		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))$
23	18 19 20 21 22	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))$
24	17 23	mpbid	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - j \in (M \dots N)$
25	16 24	eqeltrd	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to k \in (M \dots N)$
26		oveq2	$⊢ k = K - j \to K - k = K - (K - j)$
27	26	ad2antll	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - k = K - (K - j)$
28	1	zcnd	$⊢ φ \to K \in ℂ$
29	28	adantr	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K \in ℂ$
30	9	zcnd	$⊢ j \in (K - N \dots K - M) \to j \in ℂ$
31	30	ad2antrl	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j \in ℂ$
32	29 31	nncand	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to K - (K - j) = j$
33	27 32	eqtr2d	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to j = K - k$
34	25 33	jca	$⊢ (φ \land (j \in (K - N \dots K - M) \land k = K - j)) \to (k \in (M \dots N) \land j = K - k)$
35		simprr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to j = K - k$
36		simprl	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k \in (M \dots N)$
37	2	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to M \in ℤ$
38	3	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to N \in ℤ$
39	1	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K \in ℤ$
40	13	ad2antrl	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k \in ℤ$
41		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))$
42	37 38 39 40 41	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))$
43	36 42	mpbid	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - k \in (K - N \dots K - M)$
44	35 43	eqeltrd	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to j \in (K - N \dots K - M)$
45		oveq2	$⊢ j = K - k \to K - j = K - (K - k)$
46	45	ad2antll	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - j = K - (K - k)$
47	28	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K \in ℂ$
48	13	zcnd	$⊢ k \in (M \dots N) \to k \in ℂ$
49	48	ad2antrl	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k \in ℂ$
50	47 49	nncand	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to K - (K - k) = k$
51	46 50	eqtr2d	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to k = K - j$
52	44 51	jca	$⊢ (φ \land (k \in (M \dots N) \land j = K - k)) \to (j \in (K - N \dots K - M) \land k = K - j)$
53	34 52	impbida	$⊢ φ \to ((j \in (K - N \dots K - M) \land k = K - j) \leftrightarrow (k \in (M \dots N) \land j = K - k))$
54	7 11 15 53	f1od	$⊢ φ \to (j \in (K - N \dots K - M) ⟼ K - j) : (K - N \dots K - M) \underset{1-1 onto}{⟶} (M \dots N)$
55		oveq2	$⊢ j = k \to K - j = K - k$
56		ovex	$⊢ K - k \in V$
57	55 7 56	fvmpt	$⊢ k \in (K - N \dots K - M) \to (j \in (K - N \dots K - M) ⟼ K - j) (k) = K - k$
58	57	adantl	$⊢ (φ \land k \in (K - N \dots K - M)) \to (j \in (K - N \dots K - M) ⟼ K - j) (k) = K - k$
59	5 6 54 58 4	fprodf1o	$⊢ φ \to \prod_{j = M}^{N} A = \prod_{k = K - N}^{K - M} B$

Metamath Proof Explorer

Theorem fprodrev

Proof