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 Z = M
clim2div.2 φ N Z
clim2div.3 φ k Z F k
clim2div.4 φ seq M × F A
clim2div.5 φ seq M × F N 0
Assertion clim2div φ seq N + 1 × F A seq M × F N

Proof

Step Hyp Ref Expression
1 clim2div.1 Z = M
2 clim2div.2 φ N Z
3 clim2div.3 φ k Z F k
4 clim2div.4 φ seq M × F A
5 clim2div.5 φ seq M × F N 0
6 eqid N + 1 = N + 1
7 eluzelz N M N
8 7 1 eleq2s N Z N
9 2 8 syl φ N
10 9 peano2zd φ N + 1
11 eluzel2 N M M
12 11 1 eleq2s N Z M
13 2 12 syl φ M
14 1 13 3 prodf φ seq M × F : Z
15 14 2 ffvelrnd φ seq M × F N
16 15 5 reccld φ 1 seq M × F N
17 seqex seq N + 1 × F V
18 17 a1i φ seq N + 1 × F V
19 2 1 eleqtrdi φ N M
20 peano2uz N M N + 1 M
21 19 20 syl φ N + 1 M
22 21 1 eleqtrrdi φ N + 1 Z
23 1 uztrn2 N + 1 Z j N + 1 j Z
24 22 23 sylan φ j N + 1 j Z
25 14 ffvelrnda φ j Z seq M × F j
26 24 25 syldan φ j N + 1 seq M × F j
27 mulcl k x k x
28 27 adantl φ j N + 1 k x k x
29 mulass k x y k x y = k x y
30 29 adantl φ j N + 1 k x y k x y = k x y
31 simpr φ j N + 1 j N + 1
32 19 adantr φ j N + 1 N M
33 elfzuz k M j k M
34 33 1 eleqtrrdi k M j k Z
35 34 3 sylan2 φ k M j F k
36 35 adantlr φ j N + 1 k M j F k
37 28 30 31 32 36 seqsplit φ j N + 1 seq M × F j = seq M × F N seq N + 1 × F j
38 37 eqcomd φ j N + 1 seq M × F N seq N + 1 × F j = seq M × F j
39 15 adantr φ j N + 1 seq M × F N
40 1 uztrn2 N + 1 Z k N + 1 k Z
41 22 40 sylan φ k N + 1 k Z
42 41 3 syldan φ k N + 1 F k
43 6 10 42 prodf φ seq N + 1 × F : N + 1
44 43 ffvelrnda φ j N + 1 seq N + 1 × F j
45 5 adantr φ j N + 1 seq M × F N 0
46 26 39 44 45 divmuld φ j N + 1 seq M × F j seq M × F N = seq N + 1 × F j seq M × F N seq N + 1 × F j = seq M × F j
47 38 46 mpbird φ j N + 1 seq M × F j seq M × F N = seq N + 1 × F j
48 26 39 45 divrec2d φ j N + 1 seq M × F j seq M × F N = 1 seq M × F N seq M × F j
49 47 48 eqtr3d φ j N + 1 seq N + 1 × F j = 1 seq M × F N seq M × F j
50 6 10 4 16 18 26 49 climmulc2 φ seq N + 1 × F 1 seq M × F N A
51 climcl seq M × F A A
52 4 51 syl φ A
53 52 15 5 divrec2d φ A seq M × F N = 1 seq M × F N A
54 50 53 breqtrrd φ seq N + 1 × F A seq M × F N