esumdivc

Description: An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

	Ref	Expression
Hypotheses	esumdivc.a	$⊢ φ \to A \in V$
	esumdivc.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumdivc.c	$⊢ φ \to C \in ℝ^{+}$
Assertion	esumdivc	$⊢ φ \to \underset{k \in A}{\sum^{}} B \div_{𝑒} C = \underset{k \in A}{\sum^{}} (B \div_{𝑒} C)$

Proof

Step	Hyp	Ref	Expression
1		esumdivc.a	$⊢ φ \to A \in V$
2		esumdivc.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
3		esumdivc.c	$⊢ φ \to C \in ℝ^{+}$
4		1red	$⊢ φ \to 1 \in ℝ$
5	3	rpred	$⊢ φ \to C \in ℝ$
6	3	rpne0d	$⊢ φ \to C \neq 0$
7		rexdiv	$⊢ (1 \in ℝ \land C \in ℝ \land C \neq 0) \to 1 \div_{𝑒} C = \frac{1}{C}$
8	4 5 6 7	syl3anc	$⊢ φ \to 1 \div_{𝑒} C = \frac{1}{C}$
9		ioorp	$⊢ (0, +∞) = ℝ^{+}$
10		ioossico	$⊢ (0, +∞) \subseteq [0, +∞)$
11	9 10	eqsstrri	$⊢ ℝ^{+} \subseteq [0, +∞)$
12	3	rpreccld	$⊢ φ \to \frac{1}{C} \in ℝ^{+}$
13	11 12	sselid	$⊢ φ \to \frac{1}{C} \in [0, +∞)$
14	8 13	eqeltrd	$⊢ φ \to 1 \div_{𝑒} C \in [0, +∞)$
15	1 2 14	esummulc1	$⊢ φ \to \underset{k \in A}{\sum^{}} B \cdot_{𝑒} (1 \div_{𝑒} C) = \underset{k \in A}{\sum^{}} (B \cdot_{𝑒} (1 \div_{𝑒} C))$
16		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
17	2	ralrimiva	$⊢ φ \to \forall k \in A B \in [0, +∞]$
18		nfcv	$⊢ \underline{Ⅎ} k A$
19	18	esumcl	$⊢ (A \in V \land \forall k \in A B \in [0, +∞]) \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
20	1 17 19	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
21	16 20	sselid	$⊢ φ \to \underset{k \in A}{\sum^{}} B \in ℝ^{}$
22		xdivrec	$⊢ (\underset{k \in A}{\sum^{}} B \in ℝ^{} \land C \in ℝ \land C \neq 0) \to \underset{k \in A}{\sum^{}} B \div_{𝑒} C = \underset{k \in A}{\sum^{}} B \cdot_{𝑒} (1 \div_{𝑒} C)$
23	21 5 6 22	syl3anc	$⊢ φ \to \underset{k \in A}{\sum^{}} B \div_{𝑒} C = \underset{k \in A}{\sum^{}} B \cdot_{𝑒} (1 \div_{𝑒} C)$
24	16 2	sselid	$⊢ (φ \land k \in A) \to B \in ℝ^{*}$
25	5	adantr	$⊢ (φ \land k \in A) \to C \in ℝ$
26	6	adantr	$⊢ (φ \land k \in A) \to C \neq 0$
27		xdivrec	$⊢ (B \in ℝ^{*} \land C \in ℝ \land C \neq 0) \to B \div_{𝑒} C = B \cdot_{𝑒} (1 \div_{𝑒} C)$
28	24 25 26 27	syl3anc	$⊢ (φ \land k \in A) \to B \div_{𝑒} C = B \cdot_{𝑒} (1 \div_{𝑒} C)$
29	28	esumeq2dv	$⊢ φ \to \underset{k \in A}{\sum^{}} (B \div_{𝑒} C) = \underset{k \in A}{\sum^{}} (B \cdot_{𝑒} (1 \div_{𝑒} C))$
30	15 23 29	3eqtr4d	$⊢ φ \to \underset{k \in A}{\sum^{}} B \div_{𝑒} C = \underset{k \in A}{\sum^{}} (B \div_{𝑒} C)$

Metamath Proof Explorer

Theorem esumdivc

Proof