| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prodfdiv.1 | . . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 2 |  | prodfdiv.3 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) | 
| 3 |  | prodfdiv.4 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ≠ 0) | 
| 4 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) | 
| 5 | 4 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑘 → (1 / (𝐺‘𝑛)) = (1 / (𝐺‘𝑘))) | 
| 6 |  | eqid 2736 | . . . . . 6
⊢ (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))) | 
| 7 |  | ovex 7465 | . . . . . 6
⊢ (1 /
(𝐺‘𝑘)) ∈ V | 
| 8 | 5, 6, 7 | fvmpt 7015 | . . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) → ((𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) | 
| 9 | 8 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛)))‘𝑘) = (1 / (𝐺‘𝑘))) | 
| 10 | 1, 2, 3, 9 | prodfrec 15932 | . . 3
⊢ (𝜑 → (seq𝑀( · , (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))))‘𝑁) = (1 / (seq𝑀( · , 𝐺)‘𝑁))) | 
| 11 | 10 | oveq2d 7448 | . 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))))‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) | 
| 12 |  | prodfdiv.2 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) | 
| 13 |  | eleq1w 2823 | . . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) | 
| 14 | 13 | anbi2d 630 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)))) | 
| 15 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝐺‘𝑘) = (𝐺‘𝑛)) | 
| 16 | 15 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑛) ∈ ℂ)) | 
| 17 | 14, 16 | imbi12d 344 | . . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐺‘𝑛) ∈ ℂ))) | 
| 18 | 17, 2 | chvarvv 1997 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐺‘𝑛) ∈ ℂ) | 
| 19 | 15 | neeq1d 2999 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐺‘𝑘) ≠ 0 ↔ (𝐺‘𝑛) ≠ 0)) | 
| 20 | 14, 19 | imbi12d 344 | . . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐺‘𝑛) ≠ 0))) | 
| 21 | 20, 3 | chvarvv 1997 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐺‘𝑛) ≠ 0) | 
| 22 | 18, 21 | reccld 12037 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (1 / (𝐺‘𝑛)) ∈ ℂ) | 
| 23 | 22 | fmpttd 7134 | . . . 4
⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))):(𝑀...𝑁)⟶ℂ) | 
| 24 | 23 | ffvelcdmda 7103 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛)))‘𝑘) ∈ ℂ) | 
| 25 | 12, 2, 3 | divrecd 12047 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹‘𝑘) / (𝐺‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) | 
| 26 |  | prodfdiv.5 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) | 
| 27 | 9 | oveq2d 7448 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹‘𝑘) · ((𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛)))‘𝑘)) = ((𝐹‘𝑘) · (1 / (𝐺‘𝑘)))) | 
| 28 | 25, 26, 27 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · ((𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛)))‘𝑘))) | 
| 29 | 1, 12, 24, 28 | prodfmul 15927 | . 2
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , (𝑛 ∈ (𝑀...𝑁) ↦ (1 / (𝐺‘𝑛))))‘𝑁))) | 
| 30 |  | mulcl 11240 | . . . . 5
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) | 
| 31 | 30 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) | 
| 32 | 1, 12, 31 | seqcl 14064 | . . 3
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) | 
| 33 | 1, 2, 31 | seqcl 14064 | . . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) ∈ ℂ) | 
| 34 | 1, 2, 3 | prodfn0 15931 | . . 3
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) ≠ 0) | 
| 35 | 32, 33, 34 | divrecd 12047 | . 2
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁)) = ((seq𝑀( · , 𝐹)‘𝑁) · (1 / (seq𝑀( · , 𝐺)‘𝑁)))) | 
| 36 | 11, 29, 35 | 3eqtr4d 2786 | 1
⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) |