Metamath Proof Explorer


Theorem ntrivcvgmullem

Description: Lemma for ntrivcvgmul . (Contributed by Scott Fenton, 19-Dec-2017)

Ref Expression
Hypotheses ntrivcvgmullem.1 Z = M
ntrivcvgmullem.2 φ N Z
ntrivcvgmullem.3 φ P Z
ntrivcvgmullem.4 φ X 0
ntrivcvgmullem.5 φ Y 0
ntrivcvgmullem.6 φ seq N × F X
ntrivcvgmullem.7 φ seq P × G Y
ntrivcvgmullem.8 φ k Z F k
ntrivcvgmullem.9 φ k Z G k
ntrivcvgmullem.a φ N P
ntrivcvgmullem.b φ k Z H k = F k G k
Assertion ntrivcvgmullem φ q Z w w 0 seq q × H w

Proof

Step Hyp Ref Expression
1 ntrivcvgmullem.1 Z = M
2 ntrivcvgmullem.2 φ N Z
3 ntrivcvgmullem.3 φ P Z
4 ntrivcvgmullem.4 φ X 0
5 ntrivcvgmullem.5 φ Y 0
6 ntrivcvgmullem.6 φ seq N × F X
7 ntrivcvgmullem.7 φ seq P × G Y
8 ntrivcvgmullem.8 φ k Z F k
9 ntrivcvgmullem.9 φ k Z G k
10 ntrivcvgmullem.a φ N P
11 ntrivcvgmullem.b φ k Z H k = F k G k
12 eqid N = N
13 uzssz M
14 1 13 eqsstri Z
15 14 2 sselid φ N
16 14 3 sselid φ P
17 eluz N P P N N P
18 15 16 17 syl2anc φ P N N P
19 10 18 mpbird φ P N
20 1 uztrn2 N Z k N k Z
21 2 20 sylan φ k N k Z
22 21 8 syldan φ k N F k
23 12 19 6 4 22 ntrivcvgtail φ seq P × F 0 seq P × F seq P × F
24 23 simprd φ seq P × F seq P × F
25 climcl seq P × F seq P × F seq P × F
26 24 25 syl φ seq P × F
27 climcl seq P × G Y Y
28 7 27 syl φ Y
29 23 simpld φ seq P × F 0
30 26 28 29 5 mulne0d φ seq P × F Y 0
31 eqid P = P
32 seqex seq P × H V
33 32 a1i φ seq P × H V
34 1 uztrn2 P Z k P k Z
35 3 34 sylan φ k P k Z
36 35 8 syldan φ k P F k
37 31 16 36 prodf φ seq P × F : P
38 37 ffvelrnda φ j P seq P × F j
39 35 9 syldan φ k P G k
40 31 16 39 prodf φ seq P × G : P
41 40 ffvelrnda φ j P seq P × G j
42 simpr φ j P j P
43 simpll φ j P k P j φ
44 3 adantr φ j P P Z
45 elfzuz k P j k P
46 44 45 34 syl2an φ j P k P j k Z
47 43 46 8 syl2anc φ j P k P j F k
48 43 46 9 syl2anc φ j P k P j G k
49 43 46 11 syl2anc φ j P k P j H k = F k G k
50 42 47 48 49 prodfmul φ j P seq P × H j = seq P × F j seq P × G j
51 31 16 24 33 7 38 41 50 climmul φ seq P × H seq P × F Y
52 ovex seq P × F Y V
53 neeq1 w = seq P × F Y w 0 seq P × F Y 0
54 breq2 w = seq P × F Y seq P × H w seq P × H seq P × F Y
55 53 54 anbi12d w = seq P × F Y w 0 seq P × H w seq P × F Y 0 seq P × H seq P × F Y
56 52 55 spcev seq P × F Y 0 seq P × H seq P × F Y w w 0 seq P × H w
57 30 51 56 syl2anc φ w w 0 seq P × H w
58 seqeq1 q = P seq q × H = seq P × H
59 58 breq1d q = P seq q × H w seq P × H w
60 59 anbi2d q = P w 0 seq q × H w w 0 seq P × H w
61 60 exbidv q = P w w 0 seq q × H w w w 0 seq P × H w
62 61 rspcev P Z w w 0 seq P × H w q Z w w 0 seq q × H w
63 3 57 62 syl2anc φ q Z w w 0 seq q × H w