Metamath Proof Explorer


Theorem fprodcvg

Description: The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 F=kifkAB1
prodmo.2 φkAB
prodrb.3 φNM
fprodcvg.4 φAMN
Assertion fprodcvg φseqM×FseqM×FN

Proof

Step Hyp Ref Expression
1 prodmo.1 F=kifkAB1
2 prodmo.2 φkAB
3 prodrb.3 φNM
4 fprodcvg.4 φAMN
5 eqid N=N
6 eluzelz NMN
7 3 6 syl φN
8 seqex seqM×FV
9 8 a1i φseqM×FV
10 eqid M=M
11 eluzel2 NMM
12 3 11 syl φM
13 eluzelz kMk
14 13 adantl φkMk
15 iftrue kAifkAB1=B
16 15 adantl φkMkAifkAB1=B
17 2 adantlr φkMkAB
18 16 17 eqeltrd φkMkAifkAB1
19 18 ex φkMkAifkAB1
20 iffalse ¬kAifkAB1=1
21 ax-1cn 1
22 20 21 eqeltrdi ¬kAifkAB1
23 19 22 pm2.61d1 φkMifkAB1
24 1 fvmpt2 kifkAB1Fk=ifkAB1
25 14 23 24 syl2anc φkMFk=ifkAB1
26 25 23 eqeltrd φkMFk
27 10 12 26 prodf φseqM×F:M
28 27 3 ffvelrnd φseqM×FN
29 mulid1 mm1=m
30 29 adantl φnNmm1=m
31 3 adantr φnNNM
32 simpr φnNnN
33 12 adantr φnNM
34 26 adantlr φnNkMFk
35 10 33 34 prodf φnNseqM×F:M
36 35 31 ffvelrnd φnNseqM×FN
37 elfzuz mN+1nmN+1
38 eluzelz mN+1m
39 38 adantl φmN+1m
40 4 sseld φmAmMN
41 fznuz mMN¬mN+1
42 40 41 syl6 φmA¬mN+1
43 42 con2d φmN+1¬mA
44 43 imp φmN+1¬mA
45 39 44 eldifd φmN+1mA
46 fveqeq2 k=mFk=1Fm=1
47 eldifi kAk
48 eldifn kA¬kA
49 48 20 syl kAifkAB1=1
50 49 21 eqeltrdi kAifkAB1
51 47 50 24 syl2anc kAFk=ifkAB1
52 51 49 eqtrd kAFk=1
53 46 52 vtoclga mAFm=1
54 45 53 syl φmN+1Fm=1
55 37 54 sylan2 φmN+1nFm=1
56 55 adantlr φnNmN+1nFm=1
57 30 31 32 36 56 seqid2 φnNseqM×FN=seqM×Fn
58 57 eqcomd φnNseqM×Fn=seqM×FN
59 5 7 9 28 58 climconst φseqM×FseqM×FN