Step |
Hyp |
Ref |
Expression |
1 |
|
prodfdiv.1 |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
2 |
|
prodfdiv.2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
3 |
|
prodfdiv.3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ ) |
4 |
|
prodfdiv.4 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 ) |
5 |
|
prodfdiv.5 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) ) |
6 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) ) |
7 |
6
|
oveq2d |
⊢ ( 𝑛 = 𝑘 → ( 1 / ( 𝐺 ‘ 𝑛 ) ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
8 |
|
eqid |
⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) |
9 |
|
ovex |
⊢ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ V |
10 |
7 8 9
|
fvmpt |
⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
12 |
1 3 4 11
|
prodfrec |
⊢ ( 𝜑 → ( seq 𝑀 ( · , ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ) ‘ 𝑁 ) = ( 1 / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) ) |
13 |
12
|
oveq2d |
⊢ ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq 𝑀 ( · , ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( 1 / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) ) ) |
14 |
|
eleq1w |
⊢ ( 𝑘 = 𝑛 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ) |
15 |
14
|
anbi2d |
⊢ ( 𝑘 = 𝑛 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ) ) |
16 |
|
fveq2 |
⊢ ( 𝑘 = 𝑛 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑛 ) ) |
17 |
16
|
eleq1d |
⊢ ( 𝑘 = 𝑛 → ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐺 ‘ 𝑛 ) ∈ ℂ ) ) |
18 |
15 17
|
imbi12d |
⊢ ( 𝑘 = 𝑛 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ ) ) ) |
19 |
18 3
|
chvarvv |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ ) |
20 |
16
|
neeq1d |
⊢ ( 𝑘 = 𝑛 → ( ( 𝐺 ‘ 𝑘 ) ≠ 0 ↔ ( 𝐺 ‘ 𝑛 ) ≠ 0 ) ) |
21 |
15 20
|
imbi12d |
⊢ ( 𝑘 = 𝑛 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ≠ 0 ) ) ) |
22 |
21 4
|
chvarvv |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ≠ 0 ) |
23 |
19 22
|
reccld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 1 / ( 𝐺 ‘ 𝑛 ) ) ∈ ℂ ) |
24 |
23
|
fmpttd |
⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) : ( 𝑀 ... 𝑁 ) ⟶ ℂ ) |
25 |
24
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ ) |
26 |
2 3 4
|
divrecd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ) |
27 |
11
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ) |
28 |
26 5 27
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ) |
29 |
1 2 25 28
|
prodfmul |
⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq 𝑀 ( · , ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 1 / ( 𝐺 ‘ 𝑛 ) ) ) ) ‘ 𝑁 ) ) ) |
30 |
|
mulcl |
⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ ) |
31 |
30
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ ) |
32 |
1 2 31
|
seqcl |
⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ ) |
33 |
1 3 31
|
seqcl |
⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ∈ ℂ ) |
34 |
1 3 4
|
prodfn0 |
⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ≠ 0 ) |
35 |
32 33 34
|
divrecd |
⊢ ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( 1 / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) ) ) |
36 |
13 29 35
|
3eqtr4d |
⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) ) |