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	sselid	$⊢ (φ \land k \in A) \to B \in ℝ$
13	11 3	sselid	$⊢ (φ \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	sselid	$⊢ (φ \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	sselid	$⊢ (φ \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	84 110 79	cbvsum	$⊢ \sum_{k \in u} B = \sum_{j \in u} ⦋ j / k ⦌ B$
114	113	oveq1i	$⊢ \sum_{k \in u} B + (\frac{e}{2}) = \sum_{j \in u} ⦋ j / k ⦌ B + (\frac{e}{2})$
115	112 114	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})$
116	115	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})$
117	109 116	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})$
118		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})$
119		nfcv	$⊢ \underline{Ⅎ} j C$
120	119 89 92	cbvmpt	$⊢ (k \in A ⟼ C) = (j \in A ⟼ ⦋ j / k ⦌ C)$
121	120	fveq2i	$⊢ sum^((k \in A ⟼ C)) = sum^((j \in A ⟼ ⦋ j / k ⦌ C))$
122	92 119 89	cbvsum	$⊢ \sum_{k \in v} C = \sum_{j \in v} ⦋ j / k ⦌ C$
123	122	oveq1i	$⊢ \sum_{k \in v} C + (\frac{e}{2}) = \sum_{j \in v} ⦋ j / k ⦌ C + (\frac{e}{2})$
124	121 123	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})$
125	124	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})$
126	118 125	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})$
127		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 φ$
128	84 92	oveq12d	$⊢ k = j \to B + C = ⦋ j / k ⦌ B + ⦋ j / k ⦌ C$
129		nfcv	$⊢ \underline{Ⅎ} j (B + C)$
130		nfcv	$⊢ \underline{Ⅎ} k +$
131	79 130 89	nfov	$⊢ \underline{Ⅎ} k (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)$
132	128 129 131	cbvsum	$⊢ \sum_{k \in x} (B + C) = \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)$
133	132	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))$
134	133	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))$
135	134	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)) ℝ^{} <)$
136	135	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)) ℝ^{} <)$
137	136	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)) ℝ^{} <)$
138	137 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))$
139		ge0xaddcl	$⊢ (B \in [0, +∞] \land C \in [0, +∞]) \to B +_{𝑒} C \in [0, +∞]$
140	17 20 139	syl2anc	$⊢ (φ \land k \in A) \to B +_{𝑒} C \in [0, +∞]$
141	28 140	eqeltrrd	$⊢ (φ \land k \in A) \to B + C \in [0, +∞]$
142	6 1 141	sge0clmpt	$⊢ φ \to sum^((k \in A ⟼ B + C)) \in [0, +∞]$
143	138 142	eqeltrd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{j \in x} (⦋ j / k ⦌ B + ⦋ j / k ⦌ C)) ℝ^{*} <) \in [0, +∞]$
144	127 143	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, +∞]$
145	112 4	eqeltrrid	$⊢ φ \to sum^((j \in A ⟼ ⦋ j / k ⦌ B)) \in ℝ$
146	127 145	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 ℝ$
147	121 5	eqeltrrid	$⊢ φ \to sum^((j \in A ⟼ ⦋ j / k ⦌ C)) \in ℝ$
148	127 147	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 ℝ$
149	74 88 96 97 100 103 106 108 117 126 144 146 148	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$
150	112 121	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))$
151	135	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$
152	150 151	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$
153	149 152	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$
154	153	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))$
155	154	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)$
156	72 155	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$
157	156	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))$
158	157	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)$
159	68 158	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$
160	61 159	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$
161	40 59 160	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)) ℝ^{*} <)$
162	26	eqcomd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) = sum^((k \in A ⟼ B + C))$
163	43 48 25	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B + C \in [0, +∞)$
164	42 163	sge0fsummpt	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sum^((k \in x ⟼ B + C)) = \sum_{k \in x} (B + C)$
165	49	recnd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in ℂ$
166	50	recnd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to C \in ℂ$
167	42 165 166	fsumadd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) = \sum_{k \in x} B + \sum_{k \in x} C$
168	164 167	eqtrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sum^((k \in x ⟼ B + C)) = \sum_{k \in x} B + \sum_{k \in x} C$
169	42 49	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \in ℝ$
170	42 50	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \in ℝ$
171	37	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) \in ℝ$
172	38	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <) \in ℝ$
173		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
174	173	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
175		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to φ$
176		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
177	176	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to y \subseteq A$
178		simpr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in y$
179	177 178	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in A$
180	179	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in A$
181	175 180 12	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to B \in ℝ$
182	174 181	fsumrecl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℝ$
183	182	rexrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℝ^{*}$
184	183	ralrimiva	$⊢ φ \to \forall y \in (𝒫 A \cap Fin) \sum_{k \in y} B \in ℝ^{*}$
185		eqid	$⊢ (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) = (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B)$
186	185	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 ℝ^{}$
187	184 186	syl	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{*}$
188	187	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) \subseteq ℝ^{*}$
189		simpr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in (𝒫 A \cap Fin)$
190		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B = \sum_{k \in x} B$
191		sumeq1	$⊢ y = x \to \sum_{k \in y} B = \sum_{k \in x} B$
192	191	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$
193	189 190 192	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \exists y \in (𝒫 A \cap Fin) \sum_{k \in x} B = \sum_{k \in y} B$
194	169	elexd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} B \in V$
195	185 193 194	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)$
196		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) ℝ^{} <)$
197	188 195 196	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) ℝ^{*} <)$
198		nfv	$⊢ Ⅎ z φ$
199		eqid	$⊢ (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) = (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C)$
200		elinel2	$⊢ z \in (𝒫 A \cap Fin) \to z \in Fin$
201	200	adantl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to z \in Fin$
202		simpll	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to φ$
203		elpwinss	$⊢ z \in (𝒫 A \cap Fin) \to z \subseteq A$
204	203	adantr	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to z \subseteq A$
205		simpr	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to k \in z$
206	204 205	sseldd	$⊢ (z \in (𝒫 A \cap Fin) \land k \in z) \to k \in A$
207	206	adantll	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to k \in A$
208	202 207 13	syl2anc	$⊢ ((φ \land z \in (𝒫 A \cap Fin)) \land k \in z) \to C \in ℝ$
209	201 208	fsumrecl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{k \in z} C \in ℝ$
210	209	rexrd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{k \in z} C \in ℝ^{*}$
211	198 199 210	rnmptssd	$⊢ φ \to ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) \subseteq ℝ^{*}$
212	211	adantr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) \subseteq ℝ^{*}$
213		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C = \sum_{k \in x} C$
214		sumeq1	$⊢ z = x \to \sum_{k \in z} C = \sum_{k \in x} C$
215	214	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$
216	189 213 215	syl2anc	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \exists z \in (𝒫 A \cap Fin) \sum_{k \in x} C = \sum_{k \in z} C$
217	170	elexd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} C \in V$
218	199 216 217	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)$
219		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) ℝ^{} <)$
220	212 218 219	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) ℝ^{*} <)$
221	169 170 171 172 197 220	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) ℝ^{} <)$
222	168 221	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) ℝ^{} <)$
223	222	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) ℝ^{} <)$
224	6 1 141 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) ℝ^{} <))$
225	223 224	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) ℝ^{} <)$
226	162 225	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) ℝ^{*} <)$
227	40 59 161 226	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)) ℝ^{*} <)$
228	32 35 227	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)) ℝ^{*} <)$
229	26 30 228	3eqtr4d	$⊢ φ \to sum^((k \in A ⟼ B +_{𝑒} C)) = sum^((k \in A ⟼ B)) +_{𝑒} sum^((k \in A ⟼ C))$

Metamath Proof Explorer

Theorem sge0xaddlem2

Proof