Metamath Proof Explorer

Theorem ntrivcvgmullem

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

Ref Expression
Hypotheses ntrivcvgmullem.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ntrivcvgmullem.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
ntrivcvgmullem.3 ⊢ ( 𝜑 → 𝑃 ∈ 𝑍 )
ntrivcvgmullem.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
ntrivcvgmullem.5 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
ntrivcvgmullem.6 ⊢ ( 𝜑 → seq 𝑁 ( · , 𝐹 ) ⇝ 𝑋 )
ntrivcvgmullem.7 ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐺 ) ⇝ 𝑌 )
ntrivcvgmullem.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
ntrivcvgmullem.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
ntrivcvgmullem.a ⊢ ( 𝜑 → 𝑁 ≤ 𝑃 )
ntrivcvgmullem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion ntrivcvgmullem ( 𝜑 → ∃ 𝑞 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ) )

Proof

Step Hyp Ref Expression
1 ntrivcvgmullem.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ntrivcvgmullem.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 ntrivcvgmullem.3 ⊢ ( 𝜑 → 𝑃 ∈ 𝑍 )
4 ntrivcvgmullem.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
5 ntrivcvgmullem.5 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
6 ntrivcvgmullem.6 ⊢ ( 𝜑 → seq 𝑁 ( · , 𝐹 ) ⇝ 𝑋 )
7 ntrivcvgmullem.7 ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐺 ) ⇝ 𝑌 )
8 ntrivcvgmullem.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
9 ntrivcvgmullem.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
10 ntrivcvgmullem.a ⊢ ( 𝜑 → 𝑁 ≤ 𝑃 )
11 ntrivcvgmullem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
12 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
13 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
14 1 13 eqsstri ⊢ 𝑍 ⊆ ℤ
15 14 2 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 14 3 sselid ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
17 eluz ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑃 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑃 ) )
18 15 16 17 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑃 ) )
19 10 18 mpbird ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 𝑁 ) )
20 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
21 2 20 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
22 21 8 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
23 12 19 6 4 22 ntrivcvgtail ⊢ ( 𝜑 → ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑃 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) ) )
24 23 simprd ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) )
25 climcl ⊢ ( seq 𝑃 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) → ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) ∈ ℂ )
26 24 25 syl ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) ∈ ℂ )
27 climcl ⊢ ( seq 𝑃 ( · , 𝐺 ) ⇝ 𝑌 → 𝑌 ∈ ℂ )
28 7 27 syl ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
29 23 simpld ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) ≠ 0 )
30 26 28 29 5 mulne0d ⊢ ( 𝜑 → ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ≠ 0 )
31 eqid ⊢ ( ℤ≥ ‘ 𝑃 ) = ( ℤ≥ ‘ 𝑃 )
32 seqex ⊢ seq 𝑃 ( · , 𝐻 ) ∈ V
33 32 a1i ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐻 ) ∈ V )
34 1 uztrn2 ⊢ ( ( 𝑃 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑘 ∈ 𝑍 )
35 3 34 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑘 ∈ 𝑍 )
36 35 8 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑃 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
37 31 16 36 prodf ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐹 ) : ( ℤ≥ ‘ 𝑃 ) ⟶ ℂ )
38 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) → ( seq 𝑃 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
39 35 9 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
40 31 16 39 prodf ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐺 ) : ( ℤ≥ ‘ 𝑃 ) ⟶ ℂ )
41 40 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) → ( seq 𝑃 ( · , 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) )
43 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( 𝑃 ... 𝑗 ) ) → 𝜑 )
44 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑃 ∈ 𝑍 )
45 elfzuz ⊢ ( 𝑘 ∈ ( 𝑃 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑃 ) )
46 44 45 34 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( 𝑃 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
47 43 46 8 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( 𝑃 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
48 43 46 9 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( 𝑃 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
49 43 46 11 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( 𝑃 ... 𝑗 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
50 42 47 48 49 prodfmul ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑃 ) ) → ( seq 𝑃 ( · , 𝐻 ) ‘ 𝑗 ) = ( ( seq 𝑃 ( · , 𝐹 ) ‘ 𝑗 ) · ( seq 𝑃 ( · , 𝐺 ) ‘ 𝑗 ) ) )
51 31 16 24 33 7 38 41 50 climmul ⊢ ( 𝜑 → seq 𝑃 ( · , 𝐻 ) ⇝ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) )
52 ovex ⊢ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ∈ V
53 neeq1 ⊢ ( 𝑤 = ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) → ( 𝑤 ≠ 0 ↔ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ≠ 0 ) )
54 breq2 ⊢ ( 𝑤 = ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) → ( seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ↔ seq 𝑃 ( · , 𝐻 ) ⇝ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ) )
55 53 54 anbi12d ⊢ ( 𝑤 = ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) → ( ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) ↔ ( ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ) ) )
56 52 55 spcev ⊢ ( ( ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ ( ( ⇝ ‘ seq 𝑃 ( · , 𝐹 ) ) · 𝑌 ) ) → ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) )
57 30 51 56 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) )
58 seqeq1 ⊢ ( 𝑞 = 𝑃 → seq 𝑞 ( · , 𝐻 ) = seq 𝑃 ( · , 𝐻 ) )
59 58 breq1d ⊢ ( 𝑞 = 𝑃 → ( seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ↔ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) )
60 59 anbi2d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑤 ≠ 0 ∧ seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ) ↔ ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) ) )
61 60 exbidv ⊢ ( 𝑞 = 𝑃 → ( ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ) ↔ ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) ) )
62 61 rspcev ⊢ ( ( 𝑃 ∈ 𝑍 ∧ ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑃 ( · , 𝐻 ) ⇝ 𝑤 ) ) → ∃ 𝑞 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ) )
63 3 57 62 syl2anc ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝑍 ∃ 𝑤 ( 𝑤 ≠ 0 ∧ seq 𝑞 ( · , 𝐻 ) ⇝ 𝑤 ) )