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 𝑍 = ( ℤ𝑀 )
ntrivcvgmul.3 ( 𝜑 → ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
ntrivcvgmul.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
ntrivcvgmul.5 ( 𝜑 → ∃ 𝑚𝑍𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) )
ntrivcvgmul.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
ntrivcvgmul.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐹𝑘 ) · ( 𝐺𝑘 ) ) )
Assertion ntrivcvgmul ( 𝜑 → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )

Proof

Step Hyp Ref Expression
1 ntrivcvgmul.1 𝑍 = ( ℤ𝑀 )
2 ntrivcvgmul.3 ( 𝜑 → ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
3 ntrivcvgmul.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
4 ntrivcvgmul.5 ( 𝜑 → ∃ 𝑚𝑍𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) )
5 ntrivcvgmul.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
6 ntrivcvgmul.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐹𝑘 ) · ( 𝐺𝑘 ) ) )
7 exdistrv ( ∃ 𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ↔ ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) )
8 7 2rexbii ( ∃ 𝑛𝑍𝑚𝑍𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ↔ ∃ 𝑛𝑍𝑚𝑍 ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) )
9 reeanv ( ∃ 𝑛𝑍𝑚𝑍 ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ↔ ( ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ∃ 𝑚𝑍𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) )
10 8 9 bitri ( ∃ 𝑛𝑍𝑚𝑍𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ↔ ( ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ∃ 𝑚𝑍𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) )
11 2 4 10 sylanbrc ( 𝜑 → ∃ 𝑛𝑍𝑚𝑍𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) )
12 uzssz ( ℤ𝑀 ) ⊆ ℤ
13 1 12 eqsstri 𝑍 ⊆ ℤ
14 simp2l ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑛𝑍 )
15 13 14 sseldi ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑛 ∈ ℤ )
16 15 zred ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑛 ∈ ℝ )
17 simp2r ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑚𝑍 )
18 13 17 sseldi ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑚 ∈ ℤ )
19 18 zred ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑚 ∈ ℝ )
20 simpl2l ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝑛𝑍 )
21 simpl2r ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝑚𝑍 )
22 simp3ll ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑦 ≠ 0 )
23 22 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝑦 ≠ 0 )
24 simp3rl ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑧 ≠ 0 )
25 24 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝑧 ≠ 0 )
26 simp3lr ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 )
27 26 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 )
28 simp3rr ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 )
29 28 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 )
30 simpl1 ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝜑 )
31 30 3 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) ∧ 𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
32 30 5 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) ∧ 𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
33 simpr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → 𝑛𝑚 )
34 30 6 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) ∧ 𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐹𝑘 ) · ( 𝐺𝑘 ) ) )
35 1 20 21 23 25 27 29 31 32 33 34 ntrivcvgmullem ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑛𝑚 ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )
36 simpl2r ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝑚𝑍 )
37 simpl2l ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝑛𝑍 )
38 24 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝑧 ≠ 0 )
39 22 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝑦 ≠ 0 )
40 28 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 )
41 26 adantr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 )
42 simpl1 ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝜑 )
43 42 5 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) ∧ 𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
44 42 3 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) ∧ 𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
45 simpr ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → 𝑚𝑛 )
46 3 5 mulcomd ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) · ( 𝐺𝑘 ) ) = ( ( 𝐺𝑘 ) · ( 𝐹𝑘 ) ) )
47 6 46 eqtrd ( ( 𝜑𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐺𝑘 ) · ( 𝐹𝑘 ) ) )
48 42 47 sylan ( ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) ∧ 𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐺𝑘 ) · ( 𝐹𝑘 ) ) )
49 1 36 37 38 39 40 41 43 44 45 48 ntrivcvgmullem ( ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) ∧ 𝑚𝑛 ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )
50 16 19 35 49 lecasei ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )
51 50 3expia ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ) → ( ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) ) )
52 51 exlimdvv ( ( 𝜑 ∧ ( 𝑛𝑍𝑚𝑍 ) ) → ( ∃ 𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) ) )
53 52 rexlimdvva ( 𝜑 → ( ∃ 𝑛𝑍𝑚𝑍𝑦𝑧 ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) ) )
54 11 53 mpd ( 𝜑 → ∃ 𝑝𝑍𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )