# Metamath Proof Explorer

## Theorem ntrivcvgmullem

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

Ref Expression
Hypotheses ntrivcvgmullem.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
ntrivcvgmullem.2 ${⊢}{\phi }\to {N}\in {Z}$
ntrivcvgmullem.3 ${⊢}{\phi }\to {P}\in {Z}$
ntrivcvgmullem.4 ${⊢}{\phi }\to {X}\ne 0$
ntrivcvgmullem.5 ${⊢}{\phi }\to {Y}\ne 0$
ntrivcvgmullem.6 ${⊢}{\phi }\to seq{N}\left(×,{F}\right)⇝{X}$
ntrivcvgmullem.7 ${⊢}{\phi }\to seq{P}\left(×,{G}\right)⇝{Y}$
ntrivcvgmullem.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
ntrivcvgmullem.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
ntrivcvgmullem.a ${⊢}{\phi }\to {N}\le {P}$
ntrivcvgmullem.b ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
Assertion ntrivcvgmullem ${⊢}{\phi }\to \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{q}\left(×,{H}\right)⇝{w}\right)$

### Proof

Step Hyp Ref Expression
1 ntrivcvgmullem.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 ntrivcvgmullem.2 ${⊢}{\phi }\to {N}\in {Z}$
3 ntrivcvgmullem.3 ${⊢}{\phi }\to {P}\in {Z}$
4 ntrivcvgmullem.4 ${⊢}{\phi }\to {X}\ne 0$
5 ntrivcvgmullem.5 ${⊢}{\phi }\to {Y}\ne 0$
6 ntrivcvgmullem.6 ${⊢}{\phi }\to seq{N}\left(×,{F}\right)⇝{X}$
7 ntrivcvgmullem.7 ${⊢}{\phi }\to seq{P}\left(×,{G}\right)⇝{Y}$
8 ntrivcvgmullem.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
9 ntrivcvgmullem.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
10 ntrivcvgmullem.a ${⊢}{\phi }\to {N}\le {P}$
11 ntrivcvgmullem.b ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
12 eqid ${⊢}{ℤ}_{\ge {N}}={ℤ}_{\ge {N}}$
13 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
14 1 13 eqsstri ${⊢}{Z}\subseteq ℤ$
15 14 2 sseldi ${⊢}{\phi }\to {N}\in ℤ$
16 14 3 sseldi ${⊢}{\phi }\to {P}\in ℤ$
17 eluz ${⊢}\left({N}\in ℤ\wedge {P}\in ℤ\right)\to \left({P}\in {ℤ}_{\ge {N}}↔{N}\le {P}\right)$
18 15 16 17 syl2anc ${⊢}{\phi }\to \left({P}\in {ℤ}_{\ge {N}}↔{N}\le {P}\right)$
19 10 18 mpbird ${⊢}{\phi }\to {P}\in {ℤ}_{\ge {N}}$
20 1 uztrn2 ${⊢}\left({N}\in {Z}\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {k}\in {Z}$
21 2 20 sylan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {k}\in {Z}$
22 21 8 syldan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)\in ℂ$
23 12 19 6 4 22 ntrivcvgtail ${⊢}{\phi }\to \left(⇝\left(seq{P}\left(×,{F}\right)\right)\ne 0\wedge seq{P}\left(×,{F}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right)\right)$
24 23 simprd ${⊢}{\phi }\to seq{P}\left(×,{F}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right)$
25 climcl ${⊢}seq{P}\left(×,{F}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right)\to ⇝\left(seq{P}\left(×,{F}\right)\right)\in ℂ$
26 24 25 syl ${⊢}{\phi }\to ⇝\left(seq{P}\left(×,{F}\right)\right)\in ℂ$
27 climcl ${⊢}seq{P}\left(×,{G}\right)⇝{Y}\to {Y}\in ℂ$
28 7 27 syl ${⊢}{\phi }\to {Y}\in ℂ$
29 23 simpld ${⊢}{\phi }\to ⇝\left(seq{P}\left(×,{F}\right)\right)\ne 0$
30 26 28 29 5 mulne0d ${⊢}{\phi }\to ⇝\left(seq{P}\left(×,{F}\right)\right){Y}\ne 0$
31 eqid ${⊢}{ℤ}_{\ge {P}}={ℤ}_{\ge {P}}$
32 seqex ${⊢}seq{P}\left(×,{H}\right)\in \mathrm{V}$
33 32 a1i ${⊢}{\phi }\to seq{P}\left(×,{H}\right)\in \mathrm{V}$
34 1 uztrn2 ${⊢}\left({P}\in {Z}\wedge {k}\in {ℤ}_{\ge {P}}\right)\to {k}\in {Z}$
35 3 34 sylan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {P}}\right)\to {k}\in {Z}$
36 35 8 syldan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {P}}\right)\to {F}\left({k}\right)\in ℂ$
37 31 16 36 prodf ${⊢}{\phi }\to seq{P}\left(×,{F}\right):{ℤ}_{\ge {P}}⟶ℂ$
38 37 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\to seq{P}\left(×,{F}\right)\left({j}\right)\in ℂ$
39 35 9 syldan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {P}}\right)\to {G}\left({k}\right)\in ℂ$
40 31 16 39 prodf ${⊢}{\phi }\to seq{P}\left(×,{G}\right):{ℤ}_{\ge {P}}⟶ℂ$
41 40 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\to seq{P}\left(×,{G}\right)\left({j}\right)\in ℂ$
42 simpr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\to {j}\in {ℤ}_{\ge {P}}$
43 simpll ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\wedge {k}\in \left({P}\dots {j}\right)\right)\to {\phi }$
44 3 adantr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\to {P}\in {Z}$
45 elfzuz ${⊢}{k}\in \left({P}\dots {j}\right)\to {k}\in {ℤ}_{\ge {P}}$
46 44 45 34 syl2an ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\wedge {k}\in \left({P}\dots {j}\right)\right)\to {k}\in {Z}$
47 43 46 8 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\wedge {k}\in \left({P}\dots {j}\right)\right)\to {F}\left({k}\right)\in ℂ$
48 43 46 9 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\wedge {k}\in \left({P}\dots {j}\right)\right)\to {G}\left({k}\right)\in ℂ$
49 43 46 11 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\wedge {k}\in \left({P}\dots {j}\right)\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
50 42 47 48 49 prodfmul ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {P}}\right)\to seq{P}\left(×,{H}\right)\left({j}\right)=seq{P}\left(×,{F}\right)\left({j}\right)seq{P}\left(×,{G}\right)\left({j}\right)$
51 31 16 24 33 7 38 41 50 climmul ${⊢}{\phi }\to seq{P}\left(×,{H}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right){Y}$
52 ovex ${⊢}⇝\left(seq{P}\left(×,{F}\right)\right){Y}\in \mathrm{V}$
53 neeq1 ${⊢}{w}=⇝\left(seq{P}\left(×,{F}\right)\right){Y}\to \left({w}\ne 0↔⇝\left(seq{P}\left(×,{F}\right)\right){Y}\ne 0\right)$
54 breq2 ${⊢}{w}=⇝\left(seq{P}\left(×,{F}\right)\right){Y}\to \left(seq{P}\left(×,{H}\right)⇝{w}↔seq{P}\left(×,{H}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right){Y}\right)$
55 53 54 anbi12d ${⊢}{w}=⇝\left(seq{P}\left(×,{F}\right)\right){Y}\to \left(\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)↔\left(⇝\left(seq{P}\left(×,{F}\right)\right){Y}\ne 0\wedge seq{P}\left(×,{H}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right){Y}\right)\right)$
56 52 55 spcev ${⊢}\left(⇝\left(seq{P}\left(×,{F}\right)\right){Y}\ne 0\wedge seq{P}\left(×,{H}\right)⇝⇝\left(seq{P}\left(×,{F}\right)\right){Y}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)$
57 30 51 56 syl2anc ${⊢}{\phi }\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)$
58 seqeq1 ${⊢}{q}={P}\to seq{q}\left(×,{H}\right)=seq{P}\left(×,{H}\right)$
59 58 breq1d ${⊢}{q}={P}\to \left(seq{q}\left(×,{H}\right)⇝{w}↔seq{P}\left(×,{H}\right)⇝{w}\right)$
60 59 anbi2d ${⊢}{q}={P}\to \left(\left({w}\ne 0\wedge seq{q}\left(×,{H}\right)⇝{w}\right)↔\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)\right)$
61 60 exbidv ${⊢}{q}={P}\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{q}\left(×,{H}\right)⇝{w}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)\right)$
62 61 rspcev ${⊢}\left({P}\in {Z}\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{P}\left(×,{H}\right)⇝{w}\right)\right)\to \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{q}\left(×,{H}\right)⇝{w}\right)$
63 3 57 62 syl2anc ${⊢}{\phi }\to \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{q}\left(×,{H}\right)⇝{w}\right)$