sge0xaddlem1

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

	Ref	Expression
Hypotheses	sge0xaddlem1.a	$⊢ φ \to A \in V$
	sge0xaddlem1.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
	sge0xaddlem1.c	$⊢ (φ \land k \in A) \to C \in [0, +∞)$
	sge0xaddlem1.rp	$⊢ φ \to E \in ℝ^{+}$
	sge0xaddlem1.u	$⊢ φ \to U \subseteq A$
	sge0xaddlem1.ufi	$⊢ φ \to U \in Fin$
	sge0xaddlem1.7	$⊢ φ \to W \subseteq A$
	sge0xaddlem1.wfi	$⊢ φ \to W \in Fin$
	sge0xaddlem1.ltb	$⊢ φ \to sum^((k \in A ⟼ B)) < \sum_{k \in U} B + (\frac{E}{2})$
	sge0xaddlem1.ltc	$⊢ φ \to sum^((k \in A ⟼ C)) < \sum_{k \in W} C + (\frac{E}{2})$
	sge0xaddlem1.xr	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in [0, +∞]$
	sge0xaddlem1.sb	$⊢ φ \to sum^((k \in A ⟼ B)) \in ℝ$
	sge0xaddlem1.sc	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ$
Assertion	sge0xaddlem1	$⊢ φ \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$

Proof

Step	Hyp	Ref	Expression
1		sge0xaddlem1.a	$⊢ φ \to A \in V$
2		sge0xaddlem1.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
3		sge0xaddlem1.c	$⊢ (φ \land k \in A) \to C \in [0, +∞)$
4		sge0xaddlem1.rp	$⊢ φ \to E \in ℝ^{+}$
5		sge0xaddlem1.u	$⊢ φ \to U \subseteq A$
6		sge0xaddlem1.ufi	$⊢ φ \to U \in Fin$
7		sge0xaddlem1.7	$⊢ φ \to W \subseteq A$
8		sge0xaddlem1.wfi	$⊢ φ \to W \in Fin$
9		sge0xaddlem1.ltb	$⊢ φ \to sum^((k \in A ⟼ B)) < \sum_{k \in U} B + (\frac{E}{2})$
10		sge0xaddlem1.ltc	$⊢ φ \to sum^((k \in A ⟼ C)) < \sum_{k \in W} C + (\frac{E}{2})$
11		sge0xaddlem1.xr	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in [0, +∞]$
12		sge0xaddlem1.sb	$⊢ φ \to sum^((k \in A ⟼ B)) \in ℝ$
13		sge0xaddlem1.sc	$⊢ φ \to sum^((k \in A ⟼ C)) \in ℝ$
14		nfv	$⊢ Ⅎ k φ$
15	14 1 2	sge0revalmpt	$⊢ φ \to sum^((k \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <)$
16	14 1 3	sge0revalmpt	$⊢ φ \to sum^((k \in A ⟼ C)) = sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <)$
17	15 16	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) ℝ^{} <)$
18	15	eqcomd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) = sum^((k \in A ⟼ B))$
19	18 12	eqeltrd	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{k \in y} B) ℝ^{*} <) \in ℝ$
20	16 13	eqeltrrd	$⊢ φ \to sup (ran (z \in (𝒫 A \cap Fin) ⟼ \sum_{k \in z} C) ℝ^{*} <) \in ℝ$
21	19 20	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 ℝ$
22	21	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 ℝ^{*}$
23	17 22	eqeltrd	$⊢ φ \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) \in ℝ^{*}$
24		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
25	24	adantl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
26		simpll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to φ$
27		elpwinss	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
28	27	adantr	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to x \subseteq A$
29		simpr	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to k \in x$
30	28 29	sseldd	$⊢ (x \in (𝒫 A \cap Fin) \land k \in x) \to k \in A$
31	30	adantll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in A$
32		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
33	32 2	sselid	$⊢ (φ \land k \in A) \to B \in ℝ$
34	26 31 33	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in ℝ$
35	32 3	sselid	$⊢ (φ \land k \in A) \to C \in ℝ$
36	26 31 35	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to C \in ℝ$
37	34 36	readdcld	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B + C \in ℝ$
38	25 37	fsumrecl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) \in ℝ$
39	38	rexrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{k \in x} (B + C) \in ℝ^{*}$
40	39	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) \sum_{k \in x} (B + C) \in ℝ^{*}$
41		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) = (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))$
42	41	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 ℝ^{}$
43	40 42	syl	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) \subseteq ℝ^{*}$
44		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 ℝ^{*}$
45	43 44	syl	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ^{}$
46	4	rpxrd	$⊢ φ \to E \in ℝ^{*}$
47	45 46	xaddcld	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E \in ℝ^{}$
48		simpl	$⊢ (φ \land k \in U) \to φ$
49	5	sselda	$⊢ (φ \land k \in U) \to k \in A$
50	48 49 2	syl2anc	$⊢ (φ \land k \in U) \to B \in [0, +∞)$
51	32 50	sselid	$⊢ (φ \land k \in U) \to B \in ℝ$
52	6 51	fsumrecl	$⊢ φ \to \sum_{k \in U} B \in ℝ$
53	4	rpred	$⊢ φ \to E \in ℝ$
54	53	rehalfcld	$⊢ φ \to \frac{E}{2} \in ℝ$
55	52 54	readdcld	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) \in ℝ$
56	32	a1i	$⊢ (φ \land k \in W) \to [0, +∞) \subseteq ℝ$
57		simpl	$⊢ (φ \land k \in W) \to φ$
58	7	adantr	$⊢ (φ \land k \in W) \to W \subseteq A$
59		simpr	$⊢ (φ \land k \in W) \to k \in W$
60	58 59	sseldd	$⊢ (φ \land k \in W) \to k \in A$
61	57 60 3	syl2anc	$⊢ (φ \land k \in W) \to C \in [0, +∞)$
62	56 61	sseldd	$⊢ (φ \land k \in W) \to C \in ℝ$
63	8 62	fsumrecl	$⊢ φ \to \sum_{k \in W} C \in ℝ$
64	63 54	readdcld	$⊢ φ \to \sum_{k \in W} C + (\frac{E}{2}) \in ℝ$
65	55 64	readdcld	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2}) \in ℝ$
66	65	rexrd	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2}) \in ℝ^{*}$
67	12 13 55 64 9 10	ltadd12dd	$⊢ φ \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) < \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2})$
68	52	recnd	$⊢ φ \to \sum_{k \in U} B \in ℂ$
69	54	recnd	$⊢ φ \to \frac{E}{2} \in ℂ$
70	63	recnd	$⊢ φ \to \sum_{k \in W} C \in ℂ$
71	68 69 70 69	add4d	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2}) = \sum_{k \in U} B + \sum_{k \in W} C + (\frac{E}{2}) + (\frac{E}{2})$
72	53	recnd	$⊢ φ \to E \in ℂ$
73	72	2halvesd	$⊢ φ \to (\frac{E}{2}) + (\frac{E}{2}) = E$
74	73	oveq2d	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + (\frac{E}{2}) + (\frac{E}{2}) = \sum_{k \in U} B + \sum_{k \in W} C + E$
75	71 74	eqtrd	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2}) = \sum_{k \in U} B + \sum_{k \in W} C + E$
76	75 66	eqeltrrd	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + E \in ℝ^{*}$
77		pnfxr	$⊢ +∞ \in ℝ^{*}$
78	77	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
79	75 65	eqeltrrd	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + E \in ℝ$
80		ltpnf	$⊢ \sum_{k \in U} B + \sum_{k \in W} C + E \in ℝ \to \sum_{k \in U} B + \sum_{k \in W} C + E < +∞$
81	79 80	syl	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + E < +∞$
82	76 78 81	xrltled	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq +∞$
83	82	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) = +∞) \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq +∞$
84		oveq1	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E = +∞ +_{𝑒} E$
85	84	adantl	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E = +∞ +_{𝑒} E$
86	53	renemnfd	$⊢ φ \to E \neq −∞$
87		xaddpnf2	$⊢ (E \in ℝ^{*} \land E \neq −∞) \to +∞ +_{𝑒} E = +∞$
88	46 86 87	syl2anc	$⊢ φ \to +∞ +_{𝑒} E = +∞$
89	88	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) = +∞) \to +∞ +_{𝑒} E = +∞$
90	85 89	eqtr2d	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to +∞ = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E$
91	83 90	breqtrd	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E$
92		simpl	$⊢ (φ \land \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) = +∞) \to φ$
93	92 11	syl	$⊢ (φ \land \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in [0, +∞]$
94		neqne	$⊢ \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \neq +∞$
95	94	adantl	$⊢ (φ \land \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \neq +∞$
96		ge0xrre	$⊢ (sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in [0, +∞] \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \neq +∞) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ$
97	93 95 96	syl2anc	$⊢ (φ \land \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ$
98	52 63	readdcld	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C \in ℝ$
99	98	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ) \to \sum_{k \in U} B + \sum_{k \in W} C \in ℝ$
100		simpr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ$
101	53	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ) \to E \in ℝ$
102	6 8	jca	$⊢ φ \to (U \in Fin \land W \in Fin)$
103		unfi	$⊢ (U \in Fin \land W \in Fin) \to U \cup W \in Fin$
104	102 103	syl	$⊢ φ \to U \cup W \in Fin$
105		simpl	$⊢ (φ \land k \in (U \cup W)) \to φ$
106	5 7	unssd	$⊢ φ \to U \cup W \subseteq A$
107	106	adantr	$⊢ (φ \land k \in (U \cup W)) \to U \cup W \subseteq A$
108		simpr	$⊢ (φ \land k \in (U \cup W)) \to k \in (U \cup W)$
109	107 108	sseldd	$⊢ (φ \land k \in (U \cup W)) \to k \in A$
110	105 109 33	syl2anc	$⊢ (φ \land k \in (U \cup W)) \to B \in ℝ$
111	109 35	syldan	$⊢ (φ \land k \in (U \cup W)) \to C \in ℝ$
112	110 111	readdcld	$⊢ (φ \land k \in (U \cup W)) \to B + C \in ℝ$
113	104 112	fsumrecl	$⊢ φ \to \sum_{k \in U \cup W} (B + C) \in ℝ$
114	113	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ) \to \sum_{k \in U \cup W} (B + C) \in ℝ$
115	104 110	fsumrecl	$⊢ φ \to \sum_{k \in U \cup W} B \in ℝ$
116	104 111	fsumrecl	$⊢ φ \to \sum_{k \in U \cup W} C \in ℝ$
117		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
118	117 2	sselid	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
119		xrge0ge0	$⊢ B \in [0, +∞] \to 0 \leq B$
120	118 119	syl	$⊢ (φ \land k \in A) \to 0 \leq B$
121	109 120	syldan	$⊢ (φ \land k \in (U \cup W)) \to 0 \leq B$
122		ssun1	$⊢ U \subseteq U \cup W$
123	122	a1i	$⊢ φ \to U \subseteq U \cup W$
124	104 110 121 123	fsumless	$⊢ φ \to \sum_{k \in U} B \leq \sum_{k \in U \cup W} B$
125	117 3	sselid	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
126		xrge0ge0	$⊢ C \in [0, +∞] \to 0 \leq C$
127	125 126	syl	$⊢ (φ \land k \in A) \to 0 \leq C$
128	109 127	syldan	$⊢ (φ \land k \in (U \cup W)) \to 0 \leq C$
129		ssun2	$⊢ W \subseteq U \cup W$
130	129	a1i	$⊢ φ \to W \subseteq U \cup W$
131	104 111 128 130	fsumless	$⊢ φ \to \sum_{k \in W} C \leq \sum_{k \in U \cup W} C$
132	52 63 115 116 124 131	le2addd	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C \leq \sum_{k \in U \cup W} B + \sum_{k \in U \cup W} C$
133	110	recnd	$⊢ (φ \land k \in (U \cup W)) \to B \in ℂ$
134	111	recnd	$⊢ (φ \land k \in (U \cup W)) \to C \in ℂ$
135	104 133 134	fsumadd	$⊢ φ \to \sum_{k \in U \cup W} (B + C) = \sum_{k \in U \cup W} B + \sum_{k \in U \cup W} C$
136	135	eqcomd	$⊢ φ \to \sum_{k \in U \cup W} B + \sum_{k \in U \cup W} C = \sum_{k \in U \cup W} (B + C)$
137	132 136	breqtrd	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C \leq \sum_{k \in U \cup W} (B + C)$
138	137	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ) \to \sum_{k \in U} B + \sum_{k \in W} C \leq \sum_{k \in U \cup W} (B + C)$
139	43	adantr	$⊢ (φ \land sup (ran (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 ℝ^{}$
140	104 106	elpwd	$⊢ φ \to U \cup W \in 𝒫 A$
141	140 104	elind	$⊢ φ \to U \cup W \in (𝒫 A \cap Fin)$
142	113	elexd	$⊢ φ \to \sum_{k \in U \cup W} (B + C) \in V$
143		sumeq1	$⊢ x = U \cup W \to \sum_{k \in x} (B + C) = \sum_{k \in U \cup W} (B + C)$
144	41 143	elrnmpt1s	$⊢ (U \cup W \in (𝒫 A \cap Fin) \land \sum_{k \in U \cup W} (B + C) \in V) \to \sum_{k \in U \cup W} (B + C) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))$
145	141 142 144	syl2anc	$⊢ φ \to \sum_{k \in U \cup W} (B + C) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))$
146	145	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) \in ℝ) \to \sum_{k \in U \cup W} (B + C) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))$
147		supxrub	$⊢ (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) \subseteq ℝ^{} \land \sum_{k \in U \cup W} (B + C) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C))) \to \sum_{k \in U \cup W} (B + C) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <)$
148	139 146 147	syl2anc	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to \sum_{k \in U \cup W} (B + C) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <)$
149	99 114 100 138 148	letrd	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to \sum_{k \in U} B + \sum_{k \in W} C \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <)$
150	99 100 101 149	leadd1dd	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) + E$
151		rexadd	$⊢ (sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ \land E \in ℝ) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) + E$
152	100 101 151	syl2anc	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) + E$
153	152	eqcomd	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) + E = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} E$
154	150 153	breqtrd	$⊢ (φ \land sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) \in ℝ) \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E$
155	92 97 154	syl2anc	$⊢ (φ \land \neg sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) = +∞) \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{} <) +_{𝑒} E$
156	91 155	pm2.61dan	$⊢ φ \to \sum_{k \in U} B + \sum_{k \in W} C + E \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} E$
157	75 156	eqbrtrd	$⊢ φ \to \sum_{k \in U} B + (\frac{E}{2}) + \sum_{k \in W} C + (\frac{E}{2}) \leq sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} E$
158	23 66 47 67 157	xrltletrd	$⊢ φ \to sum^((k \in A ⟼ B)) + sum^((k \in A ⟼ C)) < sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{k \in x} (B + C)) ℝ^{*} <) +_{𝑒} E$
159	23 47 158	xrltled	$⊢ φ \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$

Metamath Proof Explorer

Theorem sge0xaddlem1

Proof