Step | Hyp | Ref
| Expression |
1 | | prodfdiv.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | prodfdivap.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) |
3 | | elfzuz 9930 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
4 | | prodfdivap.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0) |
5 | 3, 4 | sylan2 284 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) # 0) |
6 | | eqid 2157 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))) = (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))) |
7 | | fveq2 5470 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
8 | 7 | oveq2d 5842 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (1 / (𝐺‘𝑛)) = (1 / (𝐺‘𝑘))) |
9 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
10 | 2, 4 | recclapd 8658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 / (𝐺‘𝑘)) ∈ ℂ) |
11 | 6, 8, 9, 10 | fvmptd3 5563 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) |
12 | 3, 11 | sylan2 284 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) |
13 | 11, 10 | eqeltrd 2234 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) ∈ ℂ) |
14 | 1, 2, 5, 12, 13 | prodfrecap 11454 |
. . 3
⊢ (𝜑 → (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁) = (1 / (seq𝑀( · , 𝐺)‘𝑁))) |
15 | 14 | oveq2d 5842 |
. 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) |
16 | | prodfdivap.2 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
17 | | eleq1w 2218 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑛 ∈ (ℤ≥‘𝑀))) |
18 | 17 | anbi2d 460 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ↔ (𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)))) |
19 | | fveq2 5470 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝐺‘𝑘) = (𝐺‘𝑛)) |
20 | 19 | eleq1d 2226 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑛) ∈ ℂ)) |
21 | 18, 20 | imbi12d 233 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) ∈ ℂ))) |
22 | 21, 2 | chvarvv 1888 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) ∈ ℂ) |
23 | 19 | breq1d 3977 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) # 0 ↔ (𝐺‘𝑛) # 0)) |
24 | 18, 23 | imbi12d 233 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0) ↔ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) # 0))) |
25 | 24, 4 | chvarvv 1888 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) # 0) |
26 | 22, 25 | recclapd 8658 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1 / (𝐺‘𝑛)) ∈ ℂ) |
27 | 26 | fmpttd 5624 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))):(ℤ≥‘𝑀)⟶ℂ) |
28 | 27 | ffvelrnda 5604 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘) ∈ ℂ) |
29 | 16, 2, 4 | divrecapd 8670 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘) / (𝐺‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) |
30 | | prodfdivap.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) |
31 | 11 | oveq2d 5842 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘) · ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) |
32 | 29, 30, 31 | 3eqtr4d 2200 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · ((𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛)))‘𝑘))) |
33 | 1, 16, 28, 32 | prod3fmul 11449 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (ℤ≥‘𝑀) ↦ (1 / (𝐺‘𝑛))))‘𝑁))) |
34 | | eqid 2157 |
. . . . 5
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
35 | | eluzel2 9449 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
36 | 1, 35 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
37 | 34, 36, 16 | prodf 11446 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐹):(ℤ≥‘𝑀)⟶ℂ) |
38 | 37, 1 | ffvelrnd 5605 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
39 | 34, 36, 2 | prodf 11446 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐺):(ℤ≥‘𝑀)⟶ℂ) |
40 | 39, 1 | ffvelrnd 5605 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) ∈ ℂ) |
41 | 1, 2, 5 | prodfap0 11453 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) # 0) |
42 | 38, 40, 41 | divrecapd 8670 |
. 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) |
43 | 15, 33, 42 | 3eqtr4d 2200 |
1
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) |