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