Metamath Proof Explorer

Theorem prodfdiv

Description: The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Hypotheses prodfdiv.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
prodfdiv.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
prodfdiv.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
prodfdiv.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
prodfdiv.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) )
Assertion prodfdiv ( 𝜑 → ( seq 𝑀 ( · , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) / ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) )

Proof

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 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 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) )