Metamath Proof Explorer


Theorem 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 φ k M N F k = A
fprodser.2 φ N M
fprodser.3 φ k M N A
Assertion fprodser φ k = M N A = seq M × F N

Proof

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