Step | Hyp | Ref
| Expression |
1 | | prodfdiv.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | prodfdivap.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) |
3 | | elfzuz 9977 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
4 | | prodfdivap.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0) |
5 | 3, 4 | sylan2 284 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) # 0) |
6 | | eqid 2170 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))) = (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))) |
7 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
8 | 7 | oveq2d 5869 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (1 / (𝐺‘𝑛)) = (1 / (𝐺‘𝑘))) |
9 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
10 | 2, 4 | recclapd 8698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 / (𝐺‘𝑘)) ∈ ℂ) |
11 | 6, 8, 9, 10 | fvmptd3 5589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) |
12 | 3, 11 | sylan2 284 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) |
13 | 11, 10 | eqeltrd 2247 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) ∈ ℂ) |
14 | 1, 2, 5, 12, 13 | prodfrecap 11509 |
. . 3
⊢ (𝜑 → (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁) = (1 / (seq𝑀( · , 𝐺)‘𝑁))) |
15 | 14 | oveq2d 5869 |
. 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) |
16 | | prodfdivap.2 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
17 | | eleq1w 2231 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑛 ∈ (ℤ≥‘𝑀))) |
18 | 17 | anbi2d 461 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ↔ (𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)))) |
19 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝐺‘𝑘) = (𝐺‘𝑛)) |
20 | 19 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑛) ∈ ℂ)) |
21 | 18, 20 | imbi12d 233 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) ∈ ℂ))) |
22 | 21, 2 | chvarvv 1901 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) ∈ ℂ) |
23 | 19 | breq1d 3999 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) # 0 ↔ (𝐺‘𝑛) # 0)) |
24 | 18, 23 | imbi12d 233 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0) ↔ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) # 0))) |
25 | 24, 4 | chvarvv 1901 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) # 0) |
26 | 22, 25 | recclapd 8698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1 / (𝐺‘𝑛)) ∈ ℂ) |
27 | 26 | fmpttd 5651 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))):(ℤ≥‘𝑀)⟶ℂ) |
28 | 27 | ffvelrnda 5631 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) ∈ ℂ) |
29 | 16, 2, 4 | divrecapd 8710 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘) / (𝐺‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) |
30 | | prodfdivap.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) |
31 | 11 | oveq2d 5869 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘) · ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) |
32 | 29, 30, 31 | 3eqtr4d 2213 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘))) |
33 | 1, 16, 28, 32 | prod3fmul 11504 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁))) |
34 | | eqid 2170 |
. . . . 5
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
35 | | eluzel2 9492 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
36 | 1, 35 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
37 | 34, 36, 16 | prodf 11501 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
38 | 37, 1 | ffvelrnd 5632 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
39 | 34, 36, 2 | prodf 11501 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐺):(ℤ≥‘𝑀)⟶ℂ) |
40 | 39, 1 | ffvelrnd 5632 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) ∈ ℂ) |
41 | 1, 2, 5 | prodfap0 11508 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) # 0) |
42 | 38, 40, 41 | divrecapd 8710 |
. 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) |
43 | 15, 33, 42 | 3eqtr4d 2213 |
1
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) |