fprodser

Description: A finite product expressed in terms of a partial product of an infinite sequence. The recursive definition of a finite product follows from here. (Contributed by Scott Fenton, 14-Dec-2017)

	Ref	Expression
Hypotheses	fprodser.1	$⊢ (φ \land k \in (M \dots N)) \to F (k) = A$
	fprodser.2	$⊢ φ \to N \in ℤ_{\geq M}$
	fprodser.3	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
Assertion	fprodser	$⊢ φ \to \prod_{k = M}^{N} A = seq M (\times F) (N)$

Proof

Step	Hyp	Ref	Expression
1		fprodser.1	$⊢ (φ \land k \in (M \dots N)) \to F (k) = A$
2		fprodser.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		fprodser.3	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
4		prodfc	$⊢ \prod_{j = M}^{N} (k \in (M \dots N) ⟼ A) (j) = \prod_{k = M}^{N} A$
5		fveq2	$⊢ j = (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m) \to (k \in (M \dots N) ⟼ A) (j) = (k \in (M \dots N) ⟼ A) ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m))$
6		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
7	2 6	syl	$⊢ φ \to N \in ℤ$
8	7	zcnd	$⊢ φ \to N \in ℂ$
9		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
10	2 9	syl	$⊢ φ \to M \in ℤ$
11	10	zcnd	$⊢ φ \to M \in ℂ$
12		1cnd	$⊢ φ \to 1 \in ℂ$
13	8 11 12	subadd23d	$⊢ φ \to N - M + 1 = N + 1 - M$
14	13	eqcomd	$⊢ φ \to N + 1 - M = N - M + 1$
15		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
16	2 15	syl	$⊢ φ \to N - M \in ℕ_{0}$
17		nn0p1nn	$⊢ N - M \in ℕ_{0} \to N - M + 1 \in ℕ$
18	16 17	syl	$⊢ φ \to N - M + 1 \in ℕ$
19	14 18	eqeltrd	$⊢ φ \to N + 1 - M \in ℕ$
20	12 11	pncan3d	$⊢ φ \to 1 + M - 1 = M$
21	8 12 11	pnpncand	$⊢ φ \to N + (1 - M) + (M - 1) = N$
22	20 21	oveq12d	$⊢ φ \to (1 + M - 1 \dots N + (1 - M) + (M - 1)) = (M \dots N)$
23	22	eleq2d	$⊢ φ \to (p \in (1 + M - 1 \dots N + (1 - M) + (M - 1)) \leftrightarrow p \in (M \dots N))$
24	23	biimpa	$⊢ (φ \land p \in (1 + M - 1 \dots N + (1 - M) + (M - 1))) \to p \in (M \dots N)$
25		elfzelz	$⊢ p \in (M \dots N) \to p \in ℤ$
26	25	zcnd	$⊢ p \in (M \dots N) \to p \in ℂ$
27	26	adantl	$⊢ (φ \land p \in (M \dots N)) \to p \in ℂ$
28		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
29	10 28	syl	$⊢ φ \to M - 1 \in ℤ$
30	29	zcnd	$⊢ φ \to M - 1 \in ℂ$
31	30	adantr	$⊢ (φ \land p \in (M \dots N)) \to M - 1 \in ℂ$
32	27 31	npcand	$⊢ (φ \land p \in (M \dots N)) \to (p - (M - 1)) + M - 1 = p$
33		simpr	$⊢ (φ \land p \in (M \dots N)) \to p \in (M \dots N)$
34	32 33	eqeltrd	$⊢ (φ \land p \in (M \dots N)) \to (p - (M - 1)) + M - 1 \in (M \dots N)$
35		ovex	$⊢ p - (M - 1) \in V$
36		oveq1	$⊢ n = p - (M - 1) \to n + M - 1 = (p - (M - 1)) + M - 1$
37	36	eleq1d	$⊢ n = p - (M - 1) \to (n + M - 1 \in (M \dots N) \leftrightarrow (p - (M - 1)) + M - 1 \in (M \dots N))$
38	35 37	sbcie	$⊢ \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N) \leftrightarrow (p - (M - 1)) + M - 1 \in (M \dots N)$
39	34 38	sylibr	$⊢ (φ \land p \in (M \dots N)) \to \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N)$
40	24 39	syldan	$⊢ (φ \land p \in (1 + M - 1 \dots N + (1 - M) + (M - 1))) \to \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N)$
41	40	ralrimiva	$⊢ φ \to \forall p \in (1 + M - 1 \dots N + (1 - M) + (M - 1)) \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N)$
42		1zzd	$⊢ φ \to 1 \in ℤ$
43	19	nnzd	$⊢ φ \to N + 1 - M \in ℤ$
44		fzshftral	$⊢ (1 \in ℤ \land N + 1 - M \in ℤ \land M - 1 \in ℤ) \to (\forall n \in (1 \dots N + 1 - M) n + M - 1 \in (M \dots N) \leftrightarrow \forall p \in (1 + M - 1 \dots N + (1 - M) + (M - 1)) \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N))$
45	42 43 29 44	syl3anc	$⊢ φ \to (\forall n \in (1 \dots N + 1 - M) n + M - 1 \in (M \dots N) \leftrightarrow \forall p \in (1 + M - 1 \dots N + (1 - M) + (M - 1)) \underset{˙}{[} (p - (M - 1)) / n \underset{˙}{]} n + M - 1 \in (M \dots N))$
46	41 45	mpbird	$⊢ φ \to \forall n \in (1 \dots N + 1 - M) n + M - 1 \in (M \dots N)$
47	10	adantr	$⊢ (φ \land p \in (M \dots N)) \to M \in ℤ$
48	7	adantr	$⊢ (φ \land p \in (M \dots N)) \to N \in ℤ$
49	25	adantl	$⊢ (φ \land p \in (M \dots N)) \to p \in ℤ$
50	29	adantr	$⊢ (φ \land p \in (M \dots N)) \to M - 1 \in ℤ$
51		fzsubel	$⊢ ((M \in ℤ \land N \in ℤ) \land (p \in ℤ \land M - 1 \in ℤ)) \to (p \in (M \dots N) \leftrightarrow p - (M - 1) \in (M - (M - 1) \dots N - (M - 1)))$
52	47 48 49 50 51	syl22anc	$⊢ (φ \land p \in (M \dots N)) \to (p \in (M \dots N) \leftrightarrow p - (M - 1) \in (M - (M - 1) \dots N - (M - 1)))$
53	33 52	mpbid	$⊢ (φ \land p \in (M \dots N)) \to p - (M - 1) \in (M - (M - 1) \dots N - (M - 1))$
54	11 12	nncand	$⊢ φ \to M - (M - 1) = 1$
55	8 11 12	subsub2d	$⊢ φ \to N - (M - 1) = N + 1 - M$
56	54 55	oveq12d	$⊢ φ \to (M - (M - 1) \dots N - (M - 1)) = (1 \dots N + 1 - M)$
57	56	adantr	$⊢ (φ \land p \in (M \dots N)) \to (M - (M - 1) \dots N - (M - 1)) = (1 \dots N + 1 - M)$
58	53 57	eleqtrd	$⊢ (φ \land p \in (M \dots N)) \to p - (M - 1) \in (1 \dots N + 1 - M)$
59	32	eqcomd	$⊢ (φ \land p \in (M \dots N)) \to p = (p - (M - 1)) + M - 1$
60	36	rspceeqv	$⊢ (p - (M - 1) \in (1 \dots N + 1 - M) \land p = (p - (M - 1)) + M - 1) \to \exists n \in (1 \dots N + 1 - M) p = n + M - 1$
61	58 59 60	syl2anc	$⊢ (φ \land p \in (M \dots N)) \to \exists n \in (1 \dots N + 1 - M) p = n + M - 1$
62		elfzelz	$⊢ n \in (1 \dots N + 1 - M) \to n \in ℤ$
63	62	zcnd	$⊢ n \in (1 \dots N + 1 - M) \to n \in ℂ$
64		elfzelz	$⊢ m \in (1 \dots N + 1 - M) \to m \in ℤ$
65	64	zcnd	$⊢ m \in (1 \dots N + 1 - M) \to m \in ℂ$
66	63 65	anim12i	$⊢ (n \in (1 \dots N + 1 - M) \land m \in (1 \dots N + 1 - M)) \to (n \in ℂ \land m \in ℂ)$
67		eqtr2	$⊢ (p = n + M - 1 \land p = m + M - 1) \to n + M - 1 = m + M - 1$
68		simprl	$⊢ (φ \land (n \in ℂ \land m \in ℂ)) \to n \in ℂ$
69		simprr	$⊢ (φ \land (n \in ℂ \land m \in ℂ)) \to m \in ℂ$
70	30	adantr	$⊢ (φ \land (n \in ℂ \land m \in ℂ)) \to M - 1 \in ℂ$
71	68 69 70	addcan2d	$⊢ (φ \land (n \in ℂ \land m \in ℂ)) \to (n + M - 1 = m + M - 1 \leftrightarrow n = m)$
72	67 71	imbitrid	$⊢ (φ \land (n \in ℂ \land m \in ℂ)) \to ((p = n + M - 1 \land p = m + M - 1) \to n = m)$
73	66 72	sylan2	$⊢ (φ \land (n \in (1 \dots N + 1 - M) \land m \in (1 \dots N + 1 - M))) \to ((p = n + M - 1 \land p = m + M - 1) \to n = m)$
74	73	ralrimivva	$⊢ φ \to \forall n \in (1 \dots N + 1 - M) \forall m \in (1 \dots N + 1 - M) ((p = n + M - 1 \land p = m + M - 1) \to n = m)$
75	74	adantr	$⊢ (φ \land p \in (M \dots N)) \to \forall n \in (1 \dots N + 1 - M) \forall m \in (1 \dots N + 1 - M) ((p = n + M - 1 \land p = m + M - 1) \to n = m)$
76		oveq1	$⊢ n = m \to n + M - 1 = m + M - 1$
77	76	eqeq2d	$⊢ n = m \to (p = n + M - 1 \leftrightarrow p = m + M - 1)$
78	77	reu4	$⊢ \exists! n \in (1 \dots N + 1 - M) p = n + M - 1 \leftrightarrow (\exists n \in (1 \dots N + 1 - M) p = n + M - 1 \land \forall n \in (1 \dots N + 1 - M) \forall m \in (1 \dots N + 1 - M) ((p = n + M - 1 \land p = m + M - 1) \to n = m))$
79	61 75 78	sylanbrc	$⊢ (φ \land p \in (M \dots N)) \to \exists! n \in (1 \dots N + 1 - M) p = n + M - 1$
80	79	ralrimiva	$⊢ φ \to \forall p \in (M \dots N) \exists! n \in (1 \dots N + 1 - M) p = n + M - 1$
81		eqid	$⊢ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) = (n \in (1 \dots N + 1 - M) ⟼ n + M - 1)$
82	81	f1ompt	$⊢ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) \underset{1-1 onto}{⟶} (M \dots N) \leftrightarrow (\forall n \in (1 \dots N + 1 - M) n + M - 1 \in (M \dots N) \land \forall p \in (M \dots N) \exists! n \in (1 \dots N + 1 - M) p = n + M - 1)$
83	46 80 82	sylanbrc	$⊢ φ \to (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) \underset{1-1 onto}{⟶} (M \dots N)$
84	3	fmpttd	$⊢ φ \to (k \in (M \dots N) ⟼ A) : (M \dots N) ⟶ ℂ$
85	84	ffvelcdmda	$⊢ (φ \land j \in (M \dots N)) \to (k \in (M \dots N) ⟼ A) (j) \in ℂ$
86		simpr	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to m \in (1 \dots N + 1 - M)$
87		1zzd	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to 1 \in ℤ$
88	43	adantr	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to N + 1 - M \in ℤ$
89	64	adantl	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to m \in ℤ$
90	29	adantr	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to M - 1 \in ℤ$
91		fzaddel	$⊢ ((1 \in ℤ \land N + 1 - M \in ℤ) \land (m \in ℤ \land M - 1 \in ℤ)) \to (m \in (1 \dots N + 1 - M) \leftrightarrow m + M - 1 \in (1 + M - 1 \dots N + (1 - M) + (M - 1)))$
92	87 88 89 90 91	syl22anc	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (m \in (1 \dots N + 1 - M) \leftrightarrow m + M - 1 \in (1 + M - 1 \dots N + (1 - M) + (M - 1)))$
93	86 92	mpbid	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to m + M - 1 \in (1 + M - 1 \dots N + (1 - M) + (M - 1))$
94	22	adantr	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (1 + M - 1 \dots N + (1 - M) + (M - 1)) = (M \dots N)$
95	93 94	eleqtrd	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to m + M - 1 \in (M \dots N)$
96	1	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) = A$
97		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ (m + M - 1) / k ⦌ A$
98	97	nfeq2	$⊢ Ⅎ k F (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A$
99		fveq2	$⊢ k = m + M - 1 \to F (k) = F (m + M - 1)$
100		csbeq1a	$⊢ k = m + M - 1 \to A = ⦋ (m + M - 1) / k ⦌ A$
101	99 100	eqeq12d	$⊢ k = m + M - 1 \to (F (k) = A \leftrightarrow F (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A)$
102	98 101	rspc	$⊢ m + M - 1 \in (M \dots N) \to (\forall k \in (M \dots N) F (k) = A \to F (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A)$
103	96 102	mpan9	$⊢ (φ \land m + M - 1 \in (M \dots N)) \to F (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A$
104	95 103	syldan	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to F (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A$
105		f1of	$⊢ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) \underset{1-1 onto}{⟶} (M \dots N) \to (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) ⟶ (M \dots N)$
106	83 105	syl	$⊢ φ \to (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) ⟶ (M \dots N)$
107		fvco3	$⊢ ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) : (1 \dots N + 1 - M) ⟶ (M \dots N) \land m \in (1 \dots N + 1 - M)) \to (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1)) (m) = F ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m))$
108	106 107	sylan	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1)) (m) = F ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m))$
109		ovex	$⊢ m + M - 1 \in V$
110	76 81 109	fvmpt	$⊢ m \in (1 \dots N + 1 - M) \to (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m) = m + M - 1$
111	110	adantl	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m) = m + M - 1$
112	111	fveq2d	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to F ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m)) = F (m + M - 1)$
113	108 112	eqtrd	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1)) (m) = F (m + M - 1)$
114	111	fveq2d	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (k \in (M \dots N) ⟼ A) ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m)) = (k \in (M \dots N) ⟼ A) (m + M - 1)$
115	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
116	97	nfel1	$⊢ Ⅎ k ⦋ (m + M - 1) / k ⦌ A \in ℂ$
117	100	eleq1d	$⊢ k = m + M - 1 \to (A \in ℂ \leftrightarrow ⦋ (m + M - 1) / k ⦌ A \in ℂ)$
118	116 117	rspc	$⊢ m + M - 1 \in (M \dots N) \to (\forall k \in (M \dots N) A \in ℂ \to ⦋ (m + M - 1) / k ⦌ A \in ℂ)$
119	115 118	mpan9	$⊢ (φ \land m + M - 1 \in (M \dots N)) \to ⦋ (m + M - 1) / k ⦌ A \in ℂ$
120	95 119	syldan	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to ⦋ (m + M - 1) / k ⦌ A \in ℂ$
121		eqid	$⊢ (k \in (M \dots N) ⟼ A) = (k \in (M \dots N) ⟼ A)$
122	121	fvmpts	$⊢ (m + M - 1 \in (M \dots N) \land ⦋ (m + M - 1) / k ⦌ A \in ℂ) \to (k \in (M \dots N) ⟼ A) (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A$
123	95 120 122	syl2anc	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (k \in (M \dots N) ⟼ A) (m + M - 1) = ⦋ (m + M - 1) / k ⦌ A$
124	114 123	eqtrd	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (k \in (M \dots N) ⟼ A) ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m)) = ⦋ (m + M - 1) / k ⦌ A$
125	104 113 124	3eqtr4d	$⊢ (φ \land m \in (1 \dots N + 1 - M)) \to (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1)) (m) = (k \in (M \dots N) ⟼ A) ((n \in (1 \dots N + 1 - M) ⟼ n + M - 1) (m))$
126	5 19 83 85 125	fprod	$⊢ φ \to \prod_{j = M}^{N} (k \in (M \dots N) ⟼ A) (j) = seq 1 (\times (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1))) (N + 1 - M)$
127		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
128	19 127	eleqtrdi	$⊢ φ \to N + 1 - M \in ℤ_{\geq 1}$
129	128 29 113	seqshft2	$⊢ φ \to seq 1 (\times (F \circ (n \in (1 \dots N + 1 - M) ⟼ n + M - 1))) (N + 1 - M) = seq (1 + M - 1) (\times F) (N + (1 - M) + (M - 1))$
130	20	seqeq1d	$⊢ φ \to seq (1 + M - 1) (\times F) = seq M (\times F)$
131	130 21	fveq12d	$⊢ φ \to seq (1 + M - 1) (\times F) (N + (1 - M) + (M - 1)) = seq M (\times F) (N)$
132	126 129 131	3eqtrd	$⊢ φ \to \prod_{j = M}^{N} (k \in (M \dots N) ⟼ A) (j) = seq M (\times F) (N)$
133	4 132	eqtr3id	$⊢ φ \to \prod_{k = M}^{N} A = seq M (\times F) (N)$

Metamath Proof Explorer

Theorem fprodser

Proof