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 φkMNFk=A
fprodser.2 φNM
fprodser.3 φkMNA
Assertion fprodser φk=MNA=seqM×FN

Proof

Step Hyp Ref Expression
1 fprodser.1 φkMNFk=A
2 fprodser.2 φNM
3 fprodser.3 φkMNA
4 prodfc j=MNkMNAj=k=MNA
5 fveq2 j=n1N+1-Mn+M-1mkMNAj=kMNAn1N+1-Mn+M-1m
6 eluzelz NMN
7 2 6 syl φN
8 7 zcnd φN
9 eluzel2 NMM
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 NMNM0
16 2 15 syl φNM0
17 nn0p1nn NM0N-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+1M+M1=N
22 20 21 oveq12d φ1+M-1N+1M+M1=MN
23 22 eleq2d φp1+M-1N+1M+M1pMN
24 23 biimpa φp1+M-1N+1M+M1pMN
25 elfzelz pMNp
26 25 zcnd pMNp
27 26 adantl φpMNp
28 peano2zm MM1
29 10 28 syl φM1
30 29 zcnd φM1
31 30 adantr φpMNM1
32 27 31 npcand φpMNpM1+M-1=p
33 simpr φpMNpMN
34 32 33 eqeltrd φpMNpM1+M-1MN
35 ovex pM1V
36 oveq1 n=pM1n+M-1=pM1+M-1
37 36 eleq1d n=pM1n+M-1MNpM1+M-1MN
38 35 37 sbcie [˙pM1/n]˙n+M-1MNpM1+M-1MN
39 34 38 sylibr φpMN[˙pM1/n]˙n+M-1MN
40 24 39 syldan φp1+M-1N+1M+M1[˙pM1/n]˙n+M-1MN
41 40 ralrimiva φp1+M-1N+1M+M1[˙pM1/n]˙n+M-1MN
42 1zzd φ1
43 19 nnzd φN+1-M
44 fzshftral 1N+1-MM1n1N+1-Mn+M-1MNp1+M-1N+1M+M1[˙pM1/n]˙n+M-1MN
45 42 43 29 44 syl3anc φn1N+1-Mn+M-1MNp1+M-1N+1M+M1[˙pM1/n]˙n+M-1MN
46 41 45 mpbird φn1N+1-Mn+M-1MN
47 10 adantr φpMNM
48 7 adantr φpMNN
49 25 adantl φpMNp
50 29 adantr φpMNM1
51 fzsubel MNpM1pMNpM1MM1NM1
52 47 48 49 50 51 syl22anc φpMNpMNpM1MM1NM1
53 33 52 mpbid φpMNpM1MM1NM1
54 11 12 nncand φMM1=1
55 8 11 12 subsub2d φNM1=N+1-M
56 54 55 oveq12d φMM1NM1=1N+1-M
57 56 adantr φpMNMM1NM1=1N+1-M
58 53 57 eleqtrd φpMNpM11N+1-M
59 32 eqcomd φpMNp=pM1+M-1
60 36 rspceeqv pM11N+1-Mp=pM1+M-1n1N+1-Mp=n+M-1
61 58 59 60 syl2anc φpMNn1N+1-Mp=n+M-1
62 elfzelz n1N+1-Mn
63 62 zcnd n1N+1-Mn
64 elfzelz m1N+1-Mm
65 64 zcnd m1N+1-Mm
66 63 65 anim12i n1N+1-Mm1N+1-Mnm
67 eqtr2 p=n+M-1p=m+M-1n+M-1=m+M-1
68 simprl φnmn
69 simprr φnmm
70 30 adantr φnmM1
71 68 69 70 addcan2d φnmn+M-1=m+M-1n=m
72 67 71 syl5ib φnmp=n+M-1p=m+M-1n=m
73 66 72 sylan2 φn1N+1-Mm1N+1-Mp=n+M-1p=m+M-1n=m
74 73 ralrimivva φn1N+1-Mm1N+1-Mp=n+M-1p=m+M-1n=m
75 74 adantr φpMNn1N+1-Mm1N+1-Mp=n+M-1p=m+M-1n=m
76 oveq1 n=mn+M-1=m+M-1
77 76 eqeq2d n=mp=n+M-1p=m+M-1
78 77 reu4 ∃!n1N+1-Mp=n+M-1n1N+1-Mp=n+M-1n1N+1-Mm1N+1-Mp=n+M-1p=m+M-1n=m
79 61 75 78 sylanbrc φpMN∃!n1N+1-Mp=n+M-1
80 79 ralrimiva φpMN∃!n1N+1-Mp=n+M-1
81 eqid n1N+1-Mn+M-1=n1N+1-Mn+M-1
82 81 f1ompt n1N+1-Mn+M-1:1N+1-M1-1 ontoMNn1N+1-Mn+M-1MNpMN∃!n1N+1-Mp=n+M-1
83 46 80 82 sylanbrc φn1N+1-Mn+M-1:1N+1-M1-1 ontoMN
84 3 fmpttd φkMNA:MN
85 84 ffvelrnda φjMNkMNAj
86 simpr φm1N+1-Mm1N+1-M
87 1zzd φm1N+1-M1
88 43 adantr φm1N+1-MN+1-M
89 64 adantl φm1N+1-Mm
90 29 adantr φm1N+1-MM1
91 fzaddel 1N+1-MmM1m1N+1-Mm+M-11+M-1N+1M+M1
92 87 88 89 90 91 syl22anc φm1N+1-Mm1N+1-Mm+M-11+M-1N+1M+M1
93 86 92 mpbid φm1N+1-Mm+M-11+M-1N+1M+M1
94 22 adantr φm1N+1-M1+M-1N+1M+M1=MN
95 93 94 eleqtrd φm1N+1-Mm+M-1MN
96 1 ralrimiva φkMNFk=A
97 nfcsb1v _km+M-1/kA
98 97 nfeq2 kFm+M-1=m+M-1/kA
99 fveq2 k=m+M-1Fk=Fm+M-1
100 csbeq1a k=m+M-1A=m+M-1/kA
101 99 100 eqeq12d k=m+M-1Fk=AFm+M-1=m+M-1/kA
102 98 101 rspc m+M-1MNkMNFk=AFm+M-1=m+M-1/kA
103 96 102 mpan9 φm+M-1MNFm+M-1=m+M-1/kA
104 95 103 syldan φm1N+1-MFm+M-1=m+M-1/kA
105 f1of n1N+1-Mn+M-1:1N+1-M1-1 ontoMNn1N+1-Mn+M-1:1N+1-MMN
106 83 105 syl φn1N+1-Mn+M-1:1N+1-MMN
107 fvco3 n1N+1-Mn+M-1:1N+1-MMNm1N+1-MFn1N+1-Mn+M-1m=Fn1N+1-Mn+M-1m
108 106 107 sylan φm1N+1-MFn1N+1-Mn+M-1m=Fn1N+1-Mn+M-1m
109 ovex m+M-1V
110 76 81 109 fvmpt m1N+1-Mn1N+1-Mn+M-1m=m+M-1
111 110 adantl φm1N+1-Mn1N+1-Mn+M-1m=m+M-1
112 111 fveq2d φm1N+1-MFn1N+1-Mn+M-1m=Fm+M-1
113 108 112 eqtrd φm1N+1-MFn1N+1-Mn+M-1m=Fm+M-1
114 111 fveq2d φm1N+1-MkMNAn1N+1-Mn+M-1m=kMNAm+M-1
115 3 ralrimiva φkMNA
116 97 nfel1 km+M-1/kA
117 100 eleq1d k=m+M-1Am+M-1/kA
118 116 117 rspc m+M-1MNkMNAm+M-1/kA
119 115 118 mpan9 φm+M-1MNm+M-1/kA
120 95 119 syldan φm1N+1-Mm+M-1/kA
121 eqid kMNA=kMNA
122 121 fvmpts m+M-1MNm+M-1/kAkMNAm+M-1=m+M-1/kA
123 95 120 122 syl2anc φm1N+1-MkMNAm+M-1=m+M-1/kA
124 114 123 eqtrd φm1N+1-MkMNAn1N+1-Mn+M-1m=m+M-1/kA
125 104 113 124 3eqtr4d φm1N+1-MFn1N+1-Mn+M-1m=kMNAn1N+1-Mn+M-1m
126 5 19 83 85 125 fprod φj=MNkMNAj=seq1×Fn1N+1-Mn+M-1N+1-M
127 nnuz =1
128 19 127 eleqtrdi φN+1-M1
129 128 29 113 seqshft2 φseq1×Fn1N+1-Mn+M-1N+1-M=seq1+M-1×FN+1M+M1
130 20 seqeq1d φseq1+M-1×F=seqM×F
131 130 21 fveq12d φseq1+M-1×FN+1M+M1=seqM×FN
132 126 129 131 3eqtrd φj=MNkMNAj=seqM×FN
133 4 132 eqtr3id φk=MNA=seqM×FN