Metamath Proof Explorer

Theorem clim2div

Description: The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017)

Ref Expression
Hypotheses clim2div.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
clim2div.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
clim2div.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
clim2div.4 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 )
clim2div.5 ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
Assertion clim2div ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 clim2div.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 clim2div.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 clim2div.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4 clim2div.4 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 )
5 clim2div.5 ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
6 eqid ⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
7 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8 7 1 eleq2s ⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ )
9 2 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10 9 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
11 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12 11 1 eleq2s ⊢ ( 𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ )
13 2 12 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14 1 13 3 prodf ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )
15 14 2 ffvelrnd ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
16 15 5 reccld ⊢ ( 𝜑 → ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) ∈ ℂ )
17 seqex ⊢ seq ( 𝑁 + 1 ) ( · , 𝐹 ) ∈ V
18 17 a1i ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ∈ V )
19 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
21 19 20 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
22 21 1 eleqtrrdi ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
23 1 uztrn2 ⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
24 22 23 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
25 14 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
26 24 25 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
27 mulcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
28 27 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
29 mulass ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
32 19 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
33 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
34 33 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
35 34 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
37 28 30 31 32 36 seqsplit ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) )
39 15 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
40 1 uztrn2 ⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
41 22 40 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
42 41 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
43 6 10 42 prodf ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ )
44 43 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
45 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
46 26 39 44 45 divmuld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ↔ ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
47 38 46 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) )
48 26 39 45 divrec2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
49 47 48 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
50 6 10 4 16 18 26 49 climmulc2 ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · 𝐴 ) )
51 climcl ⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 → 𝐴 ∈ ℂ )
52 4 51 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
53 52 15 5 divrec2d ⊢ ( 𝜑 → ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · 𝐴 ) )
54 50 53 breqtrrd ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )