Theorem fprodrev

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

	Ref	Expression
Hypotheses	fprodshft.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	fprodshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fprodshft.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fprodshft.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fprodrev.5	⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → 𝐴 = 𝐵 )
Assertion	fprodrev	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fprodshft.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		fprodshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		fprodshft.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		fprodshft.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5		fprodrev.5	⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → 𝐴 = 𝐵 )
6		fzfid	⊢ ( 𝜑 → ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∈ Fin )
7		eqid	⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) = ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → 𝐾 ∈ ℤ )
9		elfzelz	⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → 𝑗 ∈ ℤ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → 𝑗 ∈ ℤ )
11	8 10	zsubcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( 𝐾 − 𝑗 ) ∈ ℤ )
12	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
13		elfzelz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
15	12 14	zsubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑘 ) ∈ ℤ )
16		simprr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
18	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑀 ∈ ℤ )
19	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑁 ∈ ℤ )
20	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝐾 ∈ ℤ )
21	9	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ℤ )
22		fzrev	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
23	18 19 20 21 22	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
24	17 23	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) )
25	16 24	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
26		oveq2	⊢ ( 𝑘 = ( 𝐾 − 𝑗 ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
27	26	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
28	1	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝐾 ∈ ℂ )
30	9	zcnd	⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → 𝑗 ∈ ℂ )
31	30	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ℂ )
32	29 31	nncand	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
33	27 32	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
34	25 33	jca	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) )
35		simprr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
36		simprl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
37	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑀 ∈ ℤ )
38	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑁 ∈ ℤ )
39	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝐾 ∈ ℤ )
40	13	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ℤ )
41		fzrev2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
42	37 38 39 40 41	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
43	36 42	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
44	35 43	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
45		oveq2	⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → ( 𝐾 − 𝑗 ) = ( 𝐾 − ( 𝐾 − 𝑘 ) ) )
46	45	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑗 ) = ( 𝐾 − ( 𝐾 − 𝑘 ) ) )
47	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝐾 ∈ ℂ )
48	13	zcnd	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℂ )
49	48	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ℂ )
50	47 49	nncand	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑘 ) ) = 𝑘 )
51	46 50	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
52	44 51	jca	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) )
53	34 52	impbida	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) )
54	7 11 15 53	f1od	⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) : ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
55		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐾 − 𝑗 ) = ( 𝐾 − 𝑘 ) )
56		ovex	⊢ ( 𝐾 − 𝑘 ) ∈ V
57	55 7 56	fvmpt	⊢ ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
58	57	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
59	5 6 54 58 4	fprodf1o	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝐵 )