sge0xaddlem2

Description: The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0xaddlem2.a	$⊢ φ \to A \in V$
	sge0xaddlem2.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
	sge0xaddlem2.c	$⊢ (φ \land k \in A) \to C \in [0, +∞)$
	sge0xaddlem2.sb	$⊢ φ \to sum^((k \in A ⟼ B)) \in ℝ$
	sge0xaddlem2.sc	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ$
Assertion	sge0xaddlem2	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		sge0xaddlem2.a	$⊢ φ \to A \in V$
2		sge0xaddlem2.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
3		sge0xaddlem2.c	$⊢ (φ \land k \in A) \to C \in [0, +∞)$
4		sge0xaddlem2.sb	$⊢ φ \to sum^((k \in A ⟼ B)) \in ℝ$
5		sge0xaddlem2.sc	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ$
6		nfv	$⊢ Ⅎ k φ$
7		0xr	$⊢ 0 \in ℝ^{*}$
8	7	a1i	$⊢ (φ \land k \in A) \to 0 \in ℝ^{*}$
9		pnfxr	$⊢ +∞ \in ℝ^{*}$
10	9	a1i	$⊢ (φ \land k \in A) \to +∞ \in ℝ^{*}$
11		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
12	11 2	sseldi	$⊢ (φ \land k \in A) \to B \in ℝ$
13	11 3	sseldi	$⊢ (φ \land k \in A) \to C \in ℝ$
14	12 13	readdcld	$⊢ (φ \land k \in A) \to B + C \in ℝ$
15	14	rexrd	$⊢ (φ \land k \in A) \to B + C \in ℝ^{*}$
16		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
17	16 2	sseldi	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
18		xrge0ge0	$⊢ B \in [0, +∞] \to 0 \leq B$
19	17 18	syl	$⊢ (φ \land k \in A) \to 0 \leq B$
20	16 3	sseldi	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
21		xrge0ge0	$⊢ C \in [0, +∞] \to 0 \leq C$
22	20 21	syl	$⊢ (φ \land k \in A) \to 0 \leq C$
23	12 13 19 22	addge0d	$⊢ (φ \land k \in A) \to 0 \leq B + C$
24	14	ltpnfd	$⊢ (φ \land k \in A) \to B + C < +∞$
25	8 10 15 23 24	elicod	$⊢ (φ \land k \in A) \to B + C \in [0, +∞)$
26	6 1 25	sge0revalmpt	$⊢ φ \to sum^((k \in A ⟼ B + C)) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <)$
27		rexadd	$⊢ (B \in ℝ \land C \in ℝ) \to B +_{𝑒} C = B + C$
28	12 13 27	syl2anc	$⊢ (φ \land k \in A) \to B +_{𝑒} C = B + C$
29	28	mpteq2dva	$⊢ φ \to (k \in A ⟼ B +_{𝑒} C) = (k \in A ⟼ B + C)$
30	29	fveq2d	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B + C))$
31		rexadd	$⊢ (sum^((k \in A ⟼ B)) \in ℝ \land sum^((k \in A ⟼ C)) \in ℝ) \to sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C))$
32	4 5 31	syl2anc	$⊢ φ \to sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C))$
33	6 1 2	sge0revalmpt	$⊢ φ \to sum^((k \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <)$
34	6 1 3	sge0revalmpt	$⊢ φ \to sum^((k \in A ⟼ C)) = sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <)$
35	33 34	oveq12d	$⊢ φ \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
36	33	eqcomd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) = sum^((k \in A ⟼ B))$
37	36 4	eqeltrd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) \in ℝ$
38	34 5	eqeltrrd	$⊢ φ \to sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <) \in ℝ$
39	37 38	readdcld	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) \in ℝ$
40	39	rexrd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) \in ℝ^{*}$
41		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
42	41	adantl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
43		simpll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to φ$
44		elpwinss	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
45	44	adantr	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to x \subseteq A$
46		simpr	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to k \in x$
47	45 46	sseldd	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to k \in A$
48	47	adantll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in A$
49	43 48 12	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in ℝ$
50	43 48 13	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to C \in ℝ$
51	49 50	readdcld	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B + C \in ℝ$
52	42 51	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) \in ℝ$
53	52	rexrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) \in ℝ^{*}$
54	53	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) \sum_{k \in x} (B + C) \in ℝ^{*}$
55		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) = (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))$
56	55	rnmptss	$⊢ \forall x \in (𝒫 A \cap Fin) \sum_{k \in x} (B + C) \in ℝ^{} \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) \subseteq ℝ^{}$
57	54 56	syl	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) \subseteq ℝ^{*}$
58		supxrcl	$⊢ ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) \subseteq ℝ^{} \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ^{*}$
59	57 58	syl	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ^{}$
60	35	eqcomd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) = sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C))$
61	60	adantr	$⊢ (φ \land e \in ℝ^{+}) \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) = sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C))$
62		nfv	$⊢ Ⅎ k (φ \land e \in ℝ^{+})$
63	1	adantr	$⊢ (φ \land e \in ℝ^{+}) \to A \in V$
64	17	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land k \in A) \to B \in [0, +∞]$
65		rphalfcl	$⊢ e \in ℝ^{+} \to \frac{e}{2} \in ℝ^{+}$
66	65	adantl	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{2} \in ℝ^{+}$
67	4	adantr	$⊢ (φ \land e \in ℝ^{+}) \to sum^((k \in A ⟼ B)) \in ℝ$
68	62 63 64 66 67	sge0ltfirpmpt2	$⊢ (φ \land e \in ℝ^{+}) \to \exists u \in (𝒫 A \cap Fin) sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})$
69	20	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land k \in A) \to C \in [0, +∞]$
70	5	adantr	$⊢ (φ \land e \in ℝ^{+}) \to sum^((k \in A ⟼ C)) \in ℝ$
71	62 63 69 66 70	sge0ltfirpmpt2	$⊢ (φ \land e \in ℝ^{+}) \to \exists v \in (𝒫 A \cap Fin) sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})$
72	71	3ad2ant1	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to \exists v \in (𝒫 A \cap Fin) sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})$
73	63	3ad2ant1	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to A \in V$
74	73	3ad2ant1	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to A \in V$
75		simpl1l	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land j \in A) \to φ$
76	75	3ad2antl1	$⊢ ((((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \land j \in A) \to φ$
77		simpr	$⊢ ((((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \land j \in A) \to j \in A$
78		nfv	$⊢ Ⅎ k (φ \land j \in A)$
79		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
80	79	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ B \in [0, +∞)$
81	78 80	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞))$
82		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
83	82	anbi2d	$⊢ k = j \to ((φ \land k \in A) \leftrightarrow (φ \land j \in A))$
84		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
85	84	eleq1d	$⊢ k = j \to (B \in [0, +∞) \leftrightarrow ⦋ j / k ⦌ B \in [0, +∞))$
86	83 85	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to B \in [0, +∞)) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)))$
87	81 86 2	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)$
88	76 77 87	syl2anc	$⊢ ((((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \land j \in A) \to ⦋ j / k ⦌ B \in [0, +∞)$
89		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ C$
90	89	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ C \in [0, +∞)$
91	78 90	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞))$
92		csbeq1a	$⊢ k = j \to C = ⦋ j / k ⦌ C$
93	92	eleq1d	$⊢ k = j \to (C \in [0, +∞) \leftrightarrow ⦋ j / k ⦌ C \in [0, +∞))$
94	83 93	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to C \in [0, +∞)) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)))$
95	91 94 3	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)$
96	76 77 95	syl2anc	$⊢ ((((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \land j \in A) \to ⦋ j / k ⦌ C \in [0, +∞)$
97		simp11r	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to e \in ℝ^{+}$
98		simp12	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to u \in (𝒫 A \cap Fin)$
99		elpwinss	$⊢ u \in (𝒫 A \cap Fin) \to u \subseteq A$
100	98 99	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to u \subseteq A$
101		elinel2	$⊢ u \in (𝒫 A \cap Fin) \to u \in Fin$
102	101	3ad2ant2	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to u \in Fin$
103	102	3ad2ant1	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to u \in Fin$
104		simp2	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to v \in (𝒫 A \cap Fin)$
105		elpwinss	$⊢ v \in (𝒫 A \cap Fin) \to v \subseteq A$
106	104 105	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to v \subseteq A$
107		elinel2	$⊢ v \in (𝒫 A \cap Fin) \to v \in Fin$
108	107	3ad2ant2	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to v \in Fin$
109		simp13	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})$
110		nfcv	$⊢ \underline{Ⅎ} j B$
111	110 79 84	cbvmpt	$⊢ (k \in A ⟼ B) = (j \in A ⟼ ⦋ j / k ⦌ B)$
112	111	fveq2i	$⊢ sum^((k \in A ⟼ B)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B))$
113		nfcv	$⊢ \underline{Ⅎ} j u$
114		nfcv	$⊢ \underline{Ⅎ} k u$
115	84 113 114 110 79	cbvsum	$⊢ \sum_{k \in u} B = \sum_{j \in u} ⦋ j / k ⦌ B$
116	115	oveq1i	$⊢ \sum_{k \in u} B + (\frac{e}{2}) = \sum_{j \in u} ⦋ j / k ⦌ B + (\frac{e}{2})$
117	112 116	breq12i	$⊢ sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2}) \leftrightarrow sum^((j \in A ⟼ ⦋ j / k ⦌ B)) < \sum_{j \in u} ⦋ j / k ⦌ B + (\frac{e}{2})$
118	117	biimpi	$⊢ sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2}) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) < \sum_{j \in u} ⦋ j / k ⦌ B + (\frac{e}{2})$
119	109 118	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) < \sum_{j \in u} ⦋ j / k ⦌ B + (\frac{e}{2})$
120		simp3	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})$
121		nfcv	$⊢ \underline{Ⅎ} j C$
122	121 89 92	cbvmpt	$⊢ (k \in A ⟼ C) = (j \in A ⟼ ⦋ j / k ⦌ C)$
123	122	fveq2i	$⊢ sum^((k \in A ⟼ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
124		nfcv	$⊢ \underline{Ⅎ} j v$
125		nfcv	$⊢ \underline{Ⅎ} k v$
126	92 124 125 121 89	cbvsum	$⊢ \sum_{k \in v} C = \sum_{j \in v} ⦋ j / k ⦌ C$
127	126	oveq1i	$⊢ \sum_{k \in v} C + (\frac{e}{2}) = \sum_{j \in v} ⦋ j / k ⦌ C + (\frac{e}{2})$
128	123 127	breq12i	$⊢ sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2}) \leftrightarrow sum^((j \in A ⟼ ⦋ j / k ⦌ C)) < \sum_{j \in v} ⦋ j / k ⦌ C + (\frac{e}{2})$
129	128	biimpi	$⊢ sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2}) \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) < \sum_{j \in v} ⦋ j / k ⦌ C + (\frac{e}{2})$
130	120 129	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) < \sum_{j \in v} ⦋ j / k ⦌ C + (\frac{e}{2})$
131		simp11l	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to φ$
132	84 92	oveq12d	$⊢ k = j \to B + C = ⦋ j / k ⦌ B + ⦋ j / k ⦌ C$
133		nfcv	$⊢ \underline{Ⅎ} j x$
134		nfcv	$⊢ \underline{Ⅎ} k x$
135		nfcv	$⊢ \underline{Ⅎ} j (B + C)$
136		nfcv	$⊢ \underline{Ⅎ} k +$
137	79 136 89	nfov	$⊢ \underline{Ⅎ} k (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)$
138	132 133 134 135 137	cbvsum	$⊢ \sum_{k \in x} (B + C) = \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)$
139	138	mpteq2i	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) = (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C))$
140	139	rneqi	$⊢ ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) = ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C))$
141	140	supeq1i	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{} <)$
142	141	eqcomi	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <)$
143	142	a1i	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <)$
144	143 26	eqtr4d	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{*} <) = sum^((k \in A ⟼ B + C))$
145		ge0xaddcl	$⊢ (B \in [0, +∞] \land C \in [0, +∞]) \to B +_{𝑒} C \in [0, +∞]$
146	17 20 145	syl2anc	$⊢ (φ \land k \in A) \to B +_{𝑒} C \in [0, +∞]$
147	28 146	eqeltrrd	$⊢ (φ \land k \in A) \to B + C \in [0, +∞]$
148	6 1 147	sge0clmpt	$⊢ φ \to sum^((k \in A ⟼ B + C)) \in [0, +∞]$
149	144 148	eqeltrd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{*} <) \in [0, +∞]$
150	131 149	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{*} <) \in [0, +∞]$
151	112 4	eqeltrrid	$⊢ φ \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) \in ℝ$
152	131 151	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) \in ℝ$
153	123 5	eqeltrrid	$⊢ φ \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \in ℝ$
154	131 153	syl	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \in ℝ$
155	74 88 96 97 100 103 106 108 119 130 150 152 154	sge0xaddlem1	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) + sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{*} <) +_{𝑒} e$
156	112 123	oveq12i	$⊢ sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ B)) + sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
157	141	oveq1i	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} e = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{} <) +_{𝑒} e$
158	156 157	breq12i	$⊢ sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} e \leftrightarrow sum^((j \in A ⟼ ⦋ j / k ⦌ B)) + sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{} <) +_{𝑒} e$
159	155 158	sylibr	$⊢ (((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \land v \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2})) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e$
160	159	3exp	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to (v \in (𝒫 A \cap Fin) \to (sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2}) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e))$
161	160	rexlimdv	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to (\exists v \in (𝒫 A \cap Fin) sum^((k \in A ⟼ C)) < \sum_{k \in v} C + (\frac{e}{2}) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e)$
162	72 161	mpd	$⊢ ((φ \land e \in ℝ^{+}) \land u \in (𝒫 A \cap Fin) \land sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2})) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e$
163	162	3exp	$⊢ (φ \land e \in ℝ^{+}) \to (u \in (𝒫 A \cap Fin) \to (sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2}) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e))$
164	163	rexlimdv	$⊢ (φ \land e \in ℝ^{+}) \to (\exists u \in (𝒫 A \cap Fin) sum^((k \in A ⟼ B)) < \sum_{k \in u} B + (\frac{e}{2}) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e)$
165	68 164	mpd	$⊢ (φ \land e \in ℝ^{+}) \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e$
166	61 165	eqbrtrd	$⊢ (φ \land e \in ℝ^{+}) \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} e$
167	40 59 166	xrlexaddrp	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <)$
168	26	eqcomd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) = sum^((k \in A ⟼ B + C))$
169	43 48 25	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B + C \in [0, +∞)$
170	42 169	sge0fsummpt	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sum^((k \in x ⟼ B + C)) = \sum_{k \in x} (B + C)$
171	49	recnd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in ℂ$
172	50	recnd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to C \in ℂ$
173	42 171 172	fsumadd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) = \sum_{k \in x} B + \sum_{k \in x} C$
174	170 173	eqtrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sum^((k \in x ⟼ B + C)) = \sum_{k \in x} B + \sum_{k \in x} C$
175	42 49	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \in ℝ$
176	42 50	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \in ℝ$
177	37	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) \in ℝ$
178	38	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <) \in ℝ$
179		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
180	179	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
181		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to φ$
182		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
183	182	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to y \subseteq A$
184		simpr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in y$
185	183 184	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in A$
186	185	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in A$
187	181 186 12	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to B \in ℝ$
188	180 187	fsumrecl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℝ$
189	188	rexrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℝ^{*}$
190	189	ralrimiva	$⊢ φ \to \forall y \in (𝒫 A \cap Fin) \sum_{k \in y} B \in ℝ^{*}$
191		eqid	$⊢ (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) = (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B)$
192	191	rnmptss	$⊢ \forall y \in (𝒫 A \cap Fin) \sum_{k \in y} B \in ℝ^{} \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{}$
193	190 192	syl	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{*}$
194	193	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{*}$
195		simpr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in (𝒫 A \cap Fin)$
196		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B = \sum_{k \in x} B$
197		sumeq1	$⊢ y = x \to \sum_{k \in y} B = \sum_{k \in x} B$
198	197	rspceeqv	$⊢ (x \in (𝒫 A \cap Fin) \land \sum_{k \in x} B = \sum_{k \in x} B) \to \exists y \in (𝒫 A \cap Fin) \sum_{k \in x} B = \sum_{k \in y} B$
199	195 196 198	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \exists y \in (𝒫 A \cap Fin) \sum_{k \in x} B = \sum_{k \in y} B$
200	175	elexd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \in V$
201	191 199 200	elrnmptd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \in ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B)$
202		supxrub	$⊢ (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{} \land \sum_{k \in x} B \in ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B)) \to \sum_{k \in x} B \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <)$
203	194 201 202	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <)$
204		nfv	$⊢ Ⅎ z φ$
205		eqid	$⊢ (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) = (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C)$
206		elinel2	$⊢ z \in (𝒫 A \cap Fin) \to z \in Fin$
207	206	adantl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to z \in Fin$
208		simpll	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to φ$
209		elpwinss	$⊢ z \in (𝒫 A \cap Fin) \to z \subseteq A$
210	209	adantr	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to z \subseteq A$
211		simpr	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to k \in z$
212	210 211	sseldd	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to k \in A$
213	212	adantll	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to k \in A$
214	208 213 13	syl2anc	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to C \in ℝ$
215	207 214	fsumrecl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{k \in z} C \in ℝ$
216	215	rexrd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{k \in z} C \in ℝ^{*}$
217	204 205 216	rnmptssd	$⊢ φ \to ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) \subseteq ℝ^{*}$
218	217	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) \subseteq ℝ^{*}$
219		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C = \sum_{k \in x} C$
220		sumeq1	$⊢ z = x \to \sum_{k \in z} C = \sum_{k \in x} C$
221	220	rspceeqv	$⊢ (x \in (𝒫 A \cap Fin) \land \sum_{k \in x} C = \sum_{k \in x} C) \to \exists z \in (𝒫 A \cap Fin) \sum_{k \in x} C = \sum_{k \in z} C$
222	195 219 221	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \exists z \in (𝒫 A \cap Fin) \sum_{k \in x} C = \sum_{k \in z} C$
223	176	elexd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \in V$
224	205 222 223	elrnmptd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \in ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C)$
225		supxrub	$⊢ (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) \subseteq ℝ^{} \land \sum_{k \in x} C \in ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C)) \to \sum_{k \in x} C \leq sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
226	218 224 225	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \leq sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <)$
227	175 176 177 178 203 226	le2addd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B + \sum_{k \in x} C \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
228	174 227	eqbrtrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sum^((k \in x ⟼ B + C)) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
229	228	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) sum^((k \in x ⟼ B + C)) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
230	6 1 147 40	sge0lefimpt	$⊢ φ \to (sum^((k \in A ⟼ B + C)) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) \leftrightarrow \forall x \in (𝒫 A \cap Fin) sum^((k \in x ⟼ B + C)) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <))$
231	229 230	mpbird	$⊢ φ \to sum^((k \in A ⟼ B + C)) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <)$
232	168 231	eqbrtrd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \leq sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <)$
233	40 59 167 232	xrletrid	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{} <) + sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <)$
234	32 35 233	3eqtrd	$⊢ φ \to sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C)) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <)$
235	26 30 234	3eqtr4d	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$

Metamath Proof Explorer

Theorem sge0xaddlem2

Proof