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 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) )
prodmo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
prodrb.3 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
fprodcvg.4 ( 𝜑𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion fprodcvg ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) )
2 prodmo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
3 prodrb.3 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
4 fprodcvg.4 ( 𝜑𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
5 eqid ( ℤ𝑁 ) = ( ℤ𝑁 )
6 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
7 3 6 syl ( 𝜑𝑁 ∈ ℤ )
8 seqex seq 𝑀 ( · , 𝐹 ) ∈ V
9 8 a1i ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ V )
10 eqid ( ℤ𝑀 ) = ( ℤ𝑀 )
11 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
12 3 11 syl ( 𝜑𝑀 ∈ ℤ )
13 eluzelz ( 𝑘 ∈ ( ℤ𝑀 ) → 𝑘 ∈ ℤ )
14 13 adantl ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → 𝑘 ∈ ℤ )
15 iftrue ( 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 1 ) = 𝐵 )
16 15 adantl ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 1 ) = 𝐵 )
17 2 adantlr ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ )
18 16 17 eqeltrd ( ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) ∧ 𝑘𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ )
19 18 ex ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ ) )
20 iffalse ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 1 ) = 1 )
21 ax-1cn 1 ∈ ℂ
22 20 21 eqeltrdi ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ )
23 19 22 pm2.61d1 ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ )
24 1 fvmpt2 ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 1 ) )
25 14 23 24 syl2anc ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 1 ) )
26 25 23 eqeltrd ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
27 10 12 26 prodf ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : ( ℤ𝑀 ) ⟶ ℂ )
28 27 3 ffvelrnd ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
29 mulid1 ( 𝑚 ∈ ℂ → ( 𝑚 · 1 ) = 𝑚 )
30 29 adantl ( ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) ∧ 𝑚 ∈ ℂ ) → ( 𝑚 · 1 ) = 𝑚 )
31 3 adantr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑁 ∈ ( ℤ𝑀 ) )
32 simpr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑛 ∈ ( ℤ𝑁 ) )
33 12 adantr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑀 ∈ ℤ )
34 26 adantlr ( ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) ∧ 𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
35 10 33 34 prodf ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → seq 𝑀 ( · , 𝐹 ) : ( ℤ𝑀 ) ⟶ ℂ )
36 35 31 ffvelrnd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
37 elfzuz ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
38 eluzelz ( 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → 𝑚 ∈ ℤ )
39 38 adantl ( ( 𝜑𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ℤ )
40 4 sseld ( 𝜑 → ( 𝑚𝐴𝑚 ∈ ( 𝑀 ... 𝑁 ) ) )
41 fznuz ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ¬ 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
42 40 41 syl6 ( 𝜑 → ( 𝑚𝐴 → ¬ 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
43 42 con2d ( 𝜑 → ( 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ¬ 𝑚𝐴 ) )
44 43 imp ( ( 𝜑𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ¬ 𝑚𝐴 )
45 39 44 eldifd ( ( 𝜑𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ( ℤ ∖ 𝐴 ) )
46 fveqeq2 ( 𝑘 = 𝑚 → ( ( 𝐹𝑘 ) = 1 ↔ ( 𝐹𝑚 ) = 1 ) )
47 eldifi ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → 𝑘 ∈ ℤ )
48 eldifn ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ¬ 𝑘𝐴 )
49 48 20 syl ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 1 ) = 1 )
50 49 21 eqeltrdi ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 1 ) ∈ ℂ )
51 47 50 24 syl2anc ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 1 ) )
52 51 49 eqtrd ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹𝑘 ) = 1 )
53 46 52 vtoclga ( 𝑚 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹𝑚 ) = 1 )
54 45 53 syl ( ( 𝜑𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹𝑚 ) = 1 )
55 37 54 sylan2 ( ( 𝜑𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹𝑚 ) = 1 )
56 55 adantlr ( ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹𝑚 ) = 1 )
57 30 31 32 36 56 seqid2 ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) )
58 57 eqcomd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )
59 5 7 9 28 58 climconst ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )