# Metamath Proof Explorer

## Theorem ntrivcvgmul

Description: The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses ntrivcvgmul.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
ntrivcvgmul.3 ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)$
ntrivcvgmul.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
ntrivcvgmul.5 ${⊢}{\phi }\to \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)$
ntrivcvgmul.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
ntrivcvgmul.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
Assertion ntrivcvgmul ${⊢}{\phi }\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)$

### Proof

Step Hyp Ref Expression
1 ntrivcvgmul.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 ntrivcvgmul.3 ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)$
3 ntrivcvgmul.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
4 ntrivcvgmul.5 ${⊢}{\phi }\to \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)$
5 ntrivcvgmul.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
6 ntrivcvgmul.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
7 exdistrv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)$
8 7 2rexbii ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)$
9 reeanv ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)↔\left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)$
10 8 9 bitri ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)↔\left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)$
11 2 4 10 sylanbrc ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)$
12 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
13 1 12 eqsstri ${⊢}{Z}\subseteq ℤ$
14 simp2l ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {n}\in {Z}$
15 13 14 sseldi ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {n}\in ℤ$
16 15 zred ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {n}\in ℝ$
17 simp2r ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {m}\in {Z}$
18 13 17 sseldi ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {m}\in ℤ$
19 18 zred ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {m}\in ℝ$
20 simpl2l ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {n}\in {Z}$
21 simpl2r ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {m}\in {Z}$
22 simp3ll ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {y}\ne 0$
23 22 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {y}\ne 0$
24 simp3rl ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to {z}\ne 0$
25 24 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {z}\ne 0$
26 simp3lr ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to seq{n}\left(×,{F}\right)⇝{y}$
27 26 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to seq{n}\left(×,{F}\right)⇝{y}$
28 simp3rr ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to seq{m}\left(×,{G}\right)⇝{z}$
29 28 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to seq{m}\left(×,{G}\right)⇝{z}$
30 simpl1 ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {\phi }$
31 30 3 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
32 30 5 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
33 simpr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to {n}\le {m}$
34 30 6 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
35 1 20 21 23 25 27 29 31 32 33 34 ntrivcvgmullem ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {n}\le {m}\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)$
36 simpl2r ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {m}\in {Z}$
37 simpl2l ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {n}\in {Z}$
38 24 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {z}\ne 0$
39 22 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {y}\ne 0$
40 28 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to seq{m}\left(×,{G}\right)⇝{z}$
41 26 adantr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to seq{n}\left(×,{F}\right)⇝{y}$
42 simpl1 ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {\phi }$
43 42 5 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
44 42 3 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
45 simpr ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to {m}\le {n}$
46 3 5 mulcomd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right){G}\left({k}\right)={G}\left({k}\right){F}\left({k}\right)$
47 6 46 eqtrd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={G}\left({k}\right){F}\left({k}\right)$
48 42 47 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={G}\left({k}\right){F}\left({k}\right)$
49 1 36 37 38 39 40 41 43 44 45 48 ntrivcvgmullem ${⊢}\left(\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\wedge {m}\le {n}\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)$
50 16 19 35 49 lecasei ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\wedge \left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)$
51 50 3expia ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\right)\to \left(\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)\right)$
52 51 exlimdvv ${⊢}\left({\phi }\wedge \left({n}\in {Z}\wedge {m}\in {Z}\right)\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)\right)$
53 52 rexlimdvva ${⊢}{\phi }\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge \left({z}\ne 0\wedge seq{m}\left(×,{G}\right)⇝{z}\right)\right)\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)\right)$
54 11 53 mpd ${⊢}{\phi }\to \exists {p}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\ne 0\wedge seq{p}\left(×,{H}\right)⇝{w}\right)$