This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ 𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑛 ∈ ℤ )
16 15 zred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ 𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑛 ∈ ℝ )
17 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ 𝑍 ) ∧ ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑧 ≠ 0 ∧ seq 𝑚 ( · , 𝐺 ) ⇝ 𝑧 ) ) ) → 𝑚 ∈ 𝑍 )
18 13 17 sselid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ 𝑍 ) ∧ ( ( 𝑦 ≠ 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 𝑝 ( · , 𝐻 ) ⇝ 𝑤 ) )