prodfdiv

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

	Ref	Expression
Hypotheses	prodfdiv.1	$⊢ φ \to N \in ℤ_{\geq M}$
	prodfdiv.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
	prodfdiv.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in ℂ$
	prodfdiv.4	$⊢ (φ \land k \in (M \dots N)) \to G (k) \neq 0$
	prodfdiv.5	$⊢ (φ \land k \in (M \dots N)) \to H (k) = \frac{F (k)}{G (k)}$
Assertion	prodfdiv	$⊢ φ \to seq M (\times H) (N) = \frac{seq M (\times F) (N)}{seq M (\times G) (N)}$

Proof

Step	Hyp	Ref	Expression
1		prodfdiv.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		prodfdiv.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
3		prodfdiv.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in ℂ$
4		prodfdiv.4	$⊢ (φ \land k \in (M \dots N)) \to G (k) \neq 0$
5		prodfdiv.5	$⊢ (φ \land k \in (M \dots N)) \to H (k) = \frac{F (k)}{G (k)}$
6		fveq2	$⊢ n = k \to G (n) = G (k)$
7	6	oveq2d	$⊢ n = k \to \frac{1}{G (n)} = \frac{1}{G (k)}$
8		eqid	$⊢ (n \in (M \dots N) ⟼ \frac{1}{G (n)}) = (n \in (M \dots N) ⟼ \frac{1}{G (n)})$
9		ovex	$⊢ \frac{1}{G (k)} \in V$
10	7 8 9	fvmpt	$⊢ k \in (M \dots N) \to (n \in (M \dots N) ⟼ \frac{1}{G (n)}) (k) = \frac{1}{G (k)}$
11	10	adantl	$⊢ (φ \land k \in (M \dots N)) \to (n \in (M \dots N) ⟼ \frac{1}{G (n)}) (k) = \frac{1}{G (k)}$
12	1 3 4 11	prodfrec	$⊢ φ \to seq M (\times (n \in (M \dots N) ⟼ \frac{1}{G (n)})) (N) = \frac{1}{seq M (\times G) (N)}$
13	12	oveq2d	$⊢ φ \to seq M (\times F) (N) seq M (\times (n \in (M \dots N) ⟼ \frac{1}{G (n)})) (N) = seq M (\times F) (N) (\frac{1}{seq M (\times G) (N)})$
14		eleq1w	$⊢ k = n \to (k \in (M \dots N) \leftrightarrow n \in (M \dots N))$
15	14	anbi2d	$⊢ k = n \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land n \in (M \dots N)))$
16		fveq2	$⊢ k = n \to G (k) = G (n)$
17	16	eleq1d	$⊢ k = n \to (G (k) \in ℂ \leftrightarrow G (n) \in ℂ)$
18	15 17	imbi12d	$⊢ k = n \to (((φ \land k \in (M \dots N)) \to G (k) \in ℂ) \leftrightarrow ((φ \land n \in (M \dots N)) \to G (n) \in ℂ))$
19	18 3	chvarvv	$⊢ (φ \land n \in (M \dots N)) \to G (n) \in ℂ$
20	16	neeq1d	$⊢ k = n \to (G (k) \neq 0 \leftrightarrow G (n) \neq 0)$
21	15 20	imbi12d	$⊢ k = n \to (((φ \land k \in (M \dots N)) \to G (k) \neq 0) \leftrightarrow ((φ \land n \in (M \dots N)) \to G (n) \neq 0))$
22	21 4	chvarvv	$⊢ (φ \land n \in (M \dots N)) \to G (n) \neq 0$
23	19 22	reccld	$⊢ (φ \land n \in (M \dots N)) \to \frac{1}{G (n)} \in ℂ$
24	23	fmpttd	$⊢ φ \to (n \in (M \dots N) ⟼ \frac{1}{G (n)}) : (M \dots N) ⟶ ℂ$
25	24	ffvelrnda	$⊢ (φ \land k \in (M \dots N)) \to (n \in (M \dots N) ⟼ \frac{1}{G (n)}) (k) \in ℂ$
26	2 3 4	divrecd	$⊢ (φ \land k \in (M \dots N)) \to \frac{F (k)}{G (k)} = F (k) (\frac{1}{G (k)})$
27	11	oveq2d	$⊢ (φ \land k \in (M \dots N)) \to F (k) (n \in (M \dots N) ⟼ \frac{1}{G (n)}) (k) = F (k) (\frac{1}{G (k)})$
28	26 5 27	3eqtr4d	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) (n \in (M \dots N) ⟼ \frac{1}{G (n)}) (k)$
29	1 2 25 28	prodfmul	$⊢ φ \to seq M (\times H) (N) = seq M (\times F) (N) seq M (\times (n \in (M \dots N) ⟼ \frac{1}{G (n)})) (N)$
30		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
31	30	adantl	$⊢ (φ \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
32	1 2 31	seqcl	$⊢ φ \to seq M (\times F) (N) \in ℂ$
33	1 3 31	seqcl	$⊢ φ \to seq M (\times G) (N) \in ℂ$
34	1 3 4	prodfn0	$⊢ φ \to seq M (\times G) (N) \neq 0$
35	32 33 34	divrecd	$⊢ φ \to \frac{seq M (\times F) (N)}{seq M (\times G) (N)} = seq M (\times F) (N) (\frac{1}{seq M (\times G) (N)})$
36	13 29 35	3eqtr4d	$⊢ φ \to seq M (\times H) (N) = \frac{seq M (\times F) (N)}{seq M (\times G) (N)}$

Metamath Proof Explorer

Theorem prodfdiv

Proof