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 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) ) )