This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
29 mulrid ⊢ ( 𝑚 ∈ ℂ → ( 𝑚 · 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 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 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )