fproddiv

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

	Ref	Expression
Hypotheses	fprodmul.1	$⊢ φ \to A \in Fin$
	fprodmul.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	fprodmul.3	$⊢ (φ \land k \in A) \to C \in ℂ$
	fproddiv.4	$⊢ (φ \land k \in A) \to C \neq 0$
Assertion	fproddiv	$⊢ φ \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$

Proof

Step	Hyp	Ref	Expression
1		fprodmul.1	$⊢ φ \to A \in Fin$
2		fprodmul.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		fprodmul.3	$⊢ (φ \land k \in A) \to C \in ℂ$
4		fproddiv.4	$⊢ (φ \land k \in A) \to C \neq 0$
5		1div1e1	$⊢ \frac{1}{1} = 1$
6	5	eqcomi	$⊢ 1 = \frac{1}{1}$
7		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} (\frac{B}{C}) = \prod_{k \in \emptyset} (\frac{B}{C})$
8		prod0	$⊢ \prod_{k \in \emptyset} (\frac{B}{C}) = 1$
9	7 8	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} (\frac{B}{C}) = 1$
10		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
11		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
12	10 11	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} B = 1$
13		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} C = \prod_{k \in \emptyset} C$
14		prod0	$⊢ \prod_{k \in \emptyset} C = 1$
15	13 14	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} C = 1$
16	12 15	oveq12d	$⊢ A = \emptyset \to \frac{\prod_{k \in A} B}{\prod_{k \in A} C} = \frac{1}{1}$
17	6 9 16	3eqtr4a	$⊢ A = \emptyset \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$
18	17	a1i	$⊢ φ \to (A = \emptyset \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C})$
19		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21	19 20	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
22	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
23		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
24	23	adantl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to f : (1 \dots \|A\|) ⟶ A$
25		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
26	22 24 25	syl2an	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
27	26	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) \in ℂ$
28	3	fmpttd	$⊢ φ \to (k \in A ⟼ C) : A ⟶ ℂ$
29		fco	$⊢ ((k \in A ⟼ C) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
30	28 24 29	syl2an	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
31	30	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) \in ℂ$
32		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
33	32 23	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
34		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
35	33 34	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
36	33	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f (n) \in A$
37		simpr	$⊢ (φ \land k \in A) \to k \in A$
38		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
39	38	fvmpt2	$⊢ (k \in A \land C \in ℂ) \to (k \in A ⟼ C) (k) = C$
40	37 3 39	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ C) (k) = C$
41	40 4	eqnetrd	$⊢ (φ \land k \in A) \to (k \in A ⟼ C) (k) \neq 0$
42	41	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ C) (k) \neq 0$
43	42	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to \forall k \in A (k \in A ⟼ C) (k) \neq 0$
44		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C) (f (n))$
45		nfcv	$⊢ \underline{Ⅎ} k 0$
46	44 45	nfne	$⊢ Ⅎ k (k \in A ⟼ C) (f (n)) \neq 0$
47		fveq2	$⊢ k = f (n) \to (k \in A ⟼ C) (k) = (k \in A ⟼ C) (f (n))$
48	47	neeq1d	$⊢ k = f (n) \to ((k \in A ⟼ C) (k) \neq 0 \leftrightarrow (k \in A ⟼ C) (f (n)) \neq 0)$
49	46 48	rspc	$⊢ f (n) \in A \to (\forall k \in A (k \in A ⟼ C) (k) \neq 0 \to (k \in A ⟼ C) (f (n)) \neq 0)$
50	36 43 49	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ C) (f (n)) \neq 0$
51	35 50	eqnetrd	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) \neq 0$
52	2 3 4	divcld	$⊢ (φ \land k \in A) \to \frac{B}{C} \in ℂ$
53		eqid	$⊢ (k \in A ⟼ \frac{B}{C}) = (k \in A ⟼ \frac{B}{C})$
54	53	fvmpt2	$⊢ (k \in A \land \frac{B}{C} \in ℂ) \to (k \in A ⟼ \frac{B}{C}) (k) = \frac{B}{C}$
55	37 52 54	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ \frac{B}{C}) (k) = \frac{B}{C}$
56		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
57	56	fvmpt2	$⊢ (k \in A \land B \in ℂ) \to (k \in A ⟼ B) (k) = B$
58	37 2 57	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
59	58 40	oveq12d	$⊢ (φ \land k \in A) \to \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)} = \frac{B}{C}$
60	55 59	eqtr4d	$⊢ (φ \land k \in A) \to (k \in A ⟼ \frac{B}{C}) (k) = \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)}$
61	60	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ \frac{B}{C}) (k) = \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)}$
62	61	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to \forall k \in A (k \in A ⟼ \frac{B}{C}) (k) = \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)}$
63		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ \frac{B}{C}) (f (n))$
64		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (n))$
65		nfcv	$⊢ \underline{Ⅎ} k \div$
66	64 65 44	nfov	$⊢ \underline{Ⅎ} k (\frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))})$
67	63 66	nfeq	$⊢ Ⅎ k (k \in A ⟼ \frac{B}{C}) (f (n)) = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))}$
68		fveq2	$⊢ k = f (n) \to (k \in A ⟼ \frac{B}{C}) (k) = (k \in A ⟼ \frac{B}{C}) (f (n))$
69		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B) (k) = (k \in A ⟼ B) (f (n))$
70	69 47	oveq12d	$⊢ k = f (n) \to \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)} = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))}$
71	68 70	eqeq12d	$⊢ k = f (n) \to ((k \in A ⟼ \frac{B}{C}) (k) = \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)} \leftrightarrow (k \in A ⟼ \frac{B}{C}) (f (n)) = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))})$
72	67 71	rspc	$⊢ f (n) \in A \to (\forall k \in A (k \in A ⟼ \frac{B}{C}) (k) = \frac{(k \in A ⟼ B) (k)}{(k \in A ⟼ C) (k)} \to (k \in A ⟼ \frac{B}{C}) (f (n)) = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))})$
73	36 62 72	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ \frac{B}{C}) (f (n)) = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))}$
74		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ \frac{B}{C}) \circ f) (n) = (k \in A ⟼ \frac{B}{C}) (f (n))$
75	33 74	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ \frac{B}{C}) \circ f) (n) = (k \in A ⟼ \frac{B}{C}) (f (n))$
76		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
77	33 76	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
78	77 35	oveq12d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to \frac{((k \in A ⟼ B) \circ f) (n)}{((k \in A ⟼ C) \circ f) (n)} = \frac{(k \in A ⟼ B) (f (n))}{(k \in A ⟼ C) (f (n))}$
79	73 75 78	3eqtr4d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ \frac{B}{C}) \circ f) (n) = \frac{((k \in A ⟼ B) \circ f) (n)}{((k \in A ⟼ C) \circ f) (n)}$
80	21 27 31 51 79	prodfdiv	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (\times ((k \in A ⟼ \frac{B}{C}) \circ f)) (\|A\|) = \frac{seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)}{seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)}$
81		fveq2	$⊢ m = f (n) \to (k \in A ⟼ \frac{B}{C}) (m) = (k \in A ⟼ \frac{B}{C}) (f (n))$
82	52	fmpttd	$⊢ φ \to (k \in A ⟼ \frac{B}{C}) : A ⟶ ℂ$
83	82	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ \frac{B}{C}) : A ⟶ ℂ$
84	83	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ \frac{B}{C}) (m) \in ℂ$
85	81 19 32 84 75	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ \frac{B}{C}) (m) = seq 1 (\times ((k \in A ⟼ \frac{B}{C}) \circ f)) (\|A\|)$
86		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (n))$
87	22	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
88	87	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
89	86 19 32 88 77	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
90		fveq2	$⊢ m = f (n) \to (k \in A ⟼ C) (m) = (k \in A ⟼ C) (f (n))$
91	28	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ C) : A ⟶ ℂ$
92	91	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ C) (m) \in ℂ$
93	90 19 32 92 35	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ C) (m) = seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)$
94	89 93	oveq12d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \frac{\prod_{m \in A} (k \in A ⟼ B) (m)}{\prod_{m \in A} (k \in A ⟼ C) (m)} = \frac{seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)}{seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)}$
95	80 85 94	3eqtr4d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ \frac{B}{C}) (m) = \frac{\prod_{m \in A} (k \in A ⟼ B) (m)}{\prod_{m \in A} (k \in A ⟼ C) (m)}$
96		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ \frac{B}{C}) (m) = \prod_{k \in A} (\frac{B}{C})$
97		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{k \in A} B$
98		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{k \in A} C$
99	97 98	oveq12i	$⊢ \frac{\prod_{m \in A} (k \in A ⟼ B) (m)}{\prod_{m \in A} (k \in A ⟼ C) (m)} = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$
100	95 96 99	3eqtr3g	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$
101	100	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C})$
102	101	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C})$
103	102	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C})$
104		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
105	1 104	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
106	18 103 105	mpjaod	$⊢ φ \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$

Metamath Proof Explorer

Theorem fproddiv

Proof