sge0split

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0split.a	$⊢ φ \to A \in V$
	sge0split.b	$⊢ φ \to B \in W$
	sge0split.u	$⊢ U = A \cup B$
	sge0split.in0	$⊢ φ \to A \cap B = \emptyset$
	sge0split.f	$⊢ φ \to F : U ⟶ [0, +∞]$
Assertion	sge0split	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		sge0split.a	$⊢ φ \to A \in V$
2		sge0split.b	$⊢ φ \to B \in W$
3		sge0split.u	$⊢ U = A \cup B$
4		sge0split.in0	$⊢ φ \to A \cap B = \emptyset$
5		sge0split.f	$⊢ φ \to F : U ⟶ [0, +∞]$
6	1	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to A \in V$
7	2	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to B \in W$
8	4	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to A \cap B = \emptyset$
9	5	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to F : U ⟶ [0, +∞]$
10		simpr	$⊢ (φ \land sum^(F) \in ℝ) \to sum^(F) \in ℝ$
11	6 7 3 8 9 10	sge0resplit	$⊢ (φ \land sum^(F) \in ℝ) \to sum^(F) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
12		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
13	1 2 12	syl2anc	$⊢ φ \to A \cup B \in V$
14	3 13	eqeltrid	$⊢ φ \to U \in V$
15	14	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to U \in V$
16	15 9 10	sge0ssre	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{A}) \in ℝ$
17	15 9 10	sge0ssre	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{B}) \in ℝ$
18		rexadd	$⊢ (sum^({F ↾}_{A}) \in ℝ \land sum^({F ↾}_{B}) \in ℝ) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
19	16 17 18	syl2anc	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
20	19	eqcomd	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{A}) + sum^({F ↾}_{B}) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
21	11 20	eqtrd	$⊢ (φ \land sum^(F) \in ℝ) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
22		simpl	$⊢ (φ \land \neg sum^(F) \in ℝ) \to φ$
23		simpr	$⊢ (φ \land \neg sum^(F) \in ℝ) \to \neg sum^(F) \in ℝ$
24	14 5	sge0repnf	$⊢ φ \to (sum^(F) \in ℝ \leftrightarrow \neg sum^(F) = +∞)$
25	24	adantr	$⊢ (φ \land \neg sum^(F) \in ℝ) \to (sum^(F) \in ℝ \leftrightarrow \neg sum^(F) = +∞)$
26	23 25	mtbid	$⊢ (φ \land \neg sum^(F) \in ℝ) \to \neg \neg sum^(F) = +∞$
27	26	notnotrd	$⊢ (φ \land \neg sum^(F) \in ℝ) \to sum^(F) = +∞$
28	14 5	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
29	28	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^(F) \in ℝ^{*}$
30		ssun1	$⊢ A \subseteq A \cup B$
31	30 3	sseqtrri	$⊢ A \subseteq U$
32	31	a1i	$⊢ φ \to A \subseteq U$
33	5 32	fssresd	$⊢ φ \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
34	1 33	sge0xrcl	$⊢ φ \to sum^({F ↾}_{A}) \in ℝ^{*}$
35		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
36		ssun2	$⊢ B \subseteq A \cup B$
37	36 3	sseqtrri	$⊢ B \subseteq U$
38	37	a1i	$⊢ φ \to B \subseteq U$
39	5 38	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
40	2 39	sge0cl	$⊢ φ \to sum^({F ↾}_{B}) \in [0, +∞]$
41	35 40	sselid	$⊢ φ \to sum^({F ↾}_{B}) \in ℝ^{*}$
42	34 41	xaddcld	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \in ℝ^{*}$
43	42	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \in ℝ^{*}$
44		pnfxr	$⊢ +∞ \in ℝ^{*}$
45		eqid	$⊢ +∞ = +∞$
46		xreqle	$⊢ (+∞ \in ℝ^{*} \land +∞ = +∞) \to +∞ \leq +∞$
47	44 45 46	mp2an	$⊢ +∞ \leq +∞$
48	47	a1i	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to +∞ \leq +∞$
49	14	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to U \in V$
50	5	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to F : U ⟶ [0, +∞]$
51		rnresss	$⊢ ran ({F ↾}_{A}) \subseteq ran F$
52	51	sseli	$⊢ +∞ \in ran ({F ↾}_{A}) \to +∞ \in ran F$
53	52	adantl	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to +∞ \in ran F$
54	49 50 53	sge0pnfval	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^(F) = +∞$
55		xrge0neqmnf	$⊢ sum^({F ↾}_{B}) \in [0, +∞] \to sum^({F ↾}_{B}) \neq −∞$
56	40 55	syl	$⊢ φ \to sum^({F ↾}_{B}) \neq −∞$
57		xaddpnf2	$⊢ (sum^({F ↾}_{B}) \in ℝ^{*} \land sum^({F ↾}_{B}) \neq −∞) \to +∞ +_{𝑒} sum^({F ↾}_{B}) = +∞$
58	41 56 57	syl2anc	$⊢ φ \to +∞ +_{𝑒} sum^({F ↾}_{B}) = +∞$
59	58	eqcomd	$⊢ φ \to +∞ = +∞ +_{𝑒} sum^({F ↾}_{B})$
60	59	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to +∞ = +∞ +_{𝑒} sum^({F ↾}_{B})$
61	1	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to A \in V$
62	33	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
63		simpr	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to +∞ \in ran ({F ↾}_{A})$
64	61 62 63	sge0pnfval	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) = +∞$
65	64	oveq1d	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = +∞ +_{𝑒} sum^({F ↾}_{B})$
66	60 54 65	3eqtr4d	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
67	66 54	eqtr3d	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = +∞$
68	54 67	breq12d	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to (sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leftrightarrow +∞ \leq +∞)$
69	48 68	mpbird	$⊢ (φ \land +∞ \in ran ({F ↾}_{A})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
70	47	a1i	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to +∞ \leq +∞$
71	14	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to U \in V$
72	5	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to F : U ⟶ [0, +∞]$
73		rnresss	$⊢ ran ({F ↾}_{B}) \subseteq ran F$
74	73	sseli	$⊢ +∞ \in ran ({F ↾}_{B}) \to +∞ \in ran F$
75	74	adantl	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to +∞ \in ran F$
76	71 72 75	sge0pnfval	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^(F) = +∞$
77	2	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to B \in W$
78	39	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
79		simpr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to +∞ \in ran ({F ↾}_{B})$
80	77 78 79	sge0pnfval	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{B}) = +∞$
81	80	oveq2d	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) +_{𝑒} +∞$
82	1 33	sge0cl	$⊢ φ \to sum^({F ↾}_{A}) \in [0, +∞]$
83		xrge0neqmnf	$⊢ sum^({F ↾}_{A}) \in [0, +∞] \to sum^({F ↾}_{A}) \neq −∞$
84	82 83	syl	$⊢ φ \to sum^({F ↾}_{A}) \neq −∞$
85		xaddpnf1	$⊢ (sum^({F ↾}_{A}) \in ℝ^{*} \land sum^({F ↾}_{A}) \neq −∞) \to sum^({F ↾}_{A}) +_{𝑒} +∞ = +∞$
86	34 84 85	syl2anc	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} +∞ = +∞$
87	86	adantr	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{A}) +_{𝑒} +∞ = +∞$
88	81 87	eqtrd	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = +∞$
89	76 88	breq12d	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to (sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leftrightarrow +∞ \leq +∞)$
90	70 89	mpbird	$⊢ (φ \land +∞ \in ran ({F ↾}_{B})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
91	90	adantlr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land +∞ \in ran ({F ↾}_{B})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
92		vex	$⊢ z \in V$
93		eqid	$⊢ (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
94	93	elrnmpt	$⊢ z \in V \to (z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 U \cap Fin) z = \sum_{y \in x} F (y))$
95	92 94	ax-mp	$⊢ z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 U \cap Fin) z = \sum_{y \in x} F (y)$
96	95	bilani	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to \exists x \in (𝒫 U \cap Fin) z = \sum_{y \in x} F (y)$
97		simp3	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin) \land z = \sum_{y \in x} F (y)) \to z = \sum_{y \in x} F (y)$
98		inss1	$⊢ (x \cap A) \cap (x \cap B) \subseteq x \cap A$
99		inss2	$⊢ x \cap A \subseteq A$
100	98 99	sstri	$⊢ (x \cap A) \cap (x \cap B) \subseteq A$
101		inss2	$⊢ (x \cap A) \cap (x \cap B) \subseteq x \cap B$
102		inss2	$⊢ x \cap B \subseteq B$
103	101 102	sstri	$⊢ (x \cap A) \cap (x \cap B) \subseteq B$
104	100 103	ssini	$⊢ (x \cap A) \cap (x \cap B) \subseteq A \cap B$
105	104	a1i	$⊢ φ \to (x \cap A) \cap (x \cap B) \subseteq A \cap B$
106	105 4	sseqtrd	$⊢ φ \to (x \cap A) \cap (x \cap B) \subseteq \emptyset$
107		ss0	$⊢ (x \cap A) \cap (x \cap B) \subseteq \emptyset \to (x \cap A) \cap (x \cap B) = \emptyset$
108	106 107	syl	$⊢ φ \to (x \cap A) \cap (x \cap B) = \emptyset$
109	108	ad3antrrr	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to (x \cap A) \cap (x \cap B) = \emptyset$
110		indi	$⊢ x \cap (A \cup B) = (x \cap A) \cup (x \cap B)$
111	110	eqcomi	$⊢ (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
112	111	a1i	$⊢ x \in (𝒫 U \cap Fin) \to (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
113	3	eqcomi	$⊢ A \cup B = U$
114	113	ineq2i	$⊢ x \cap (A \cup B) = x \cap U$
115	114	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap (A \cup B) = x \cap U$
116		elinel1	$⊢ x \in (𝒫 U \cap Fin) \to x \in 𝒫 U$
117		elpwi	$⊢ x \in 𝒫 U \to x \subseteq U$
118	116 117	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \subseteq U$
119		dfss2	$⊢ x \subseteq U \leftrightarrow x \cap U = x$
120	119	biimpi	$⊢ x \subseteq U \to x \cap U = x$
121	118 120	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap U = x$
122	112 115 121	3eqtrrd	$⊢ x \in (𝒫 U \cap Fin) \to x = (x \cap A) \cup (x \cap B)$
123	122	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x = (x \cap A) \cup (x \cap B)$
124		elinel2	$⊢ x \in (𝒫 U \cap Fin) \to x \in Fin$
125	124	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \in Fin$
126		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
127	5	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to F : U ⟶ [0, +∞]$
128		pm4.56	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \leftrightarrow \neg (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
129	128	biimpi	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
130		elun	$⊢ +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B})) \leftrightarrow (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
131	129 130	sylnibr	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}))$
132	131	adantll	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}))$
133		rnresun	$⊢ ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{A}) \cup ran ({F ↾}_{B})$
134	133	eqcomi	$⊢ ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran ({F ↾}_{(A \cup B)})$
135	134	a1i	$⊢ φ \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran ({F ↾}_{(A \cup B)})$
136	113	reseq2i	$⊢ {F ↾}_{(A \cup B)} = {F ↾}_{U}$
137	136	rneqi	$⊢ ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{U})$
138	137	a1i	$⊢ φ \to ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{U})$
139		ffn	$⊢ F : U ⟶ [0, +∞] \to F Fn U$
140		fnresdm	$⊢ F Fn U \to {F ↾}_{U} = F$
141	5 139 140	3syl	$⊢ φ \to {F ↾}_{U} = F$
142	141	rneqd	$⊢ φ \to ran ({F ↾}_{U}) = ran F$
143	135 138 142	3eqtrd	$⊢ φ \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran F$
144	143	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran F$
145	132 144	neleqtrd	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in ran F$
146	127 145	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to F : U ⟶ [0, +∞)$
147	146	ad2antrr	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F : U ⟶ [0, +∞)$
148	118	adantr	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to x \subseteq U$
149		simpr	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in x$
150	148 149	sseldd	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in U$
151	150	adantll	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in x) \to y \in U$
152	147 151	ffvelcdmd	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
153	126 152	sselid	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in ℝ$
154	153	recnd	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in ℂ$
155	109 123 125 154	fsumsplit	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x} F (y) = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
156		infi	$⊢ x \in Fin \to x \cap A \in Fin$
157	124 156	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in Fin$
158	157	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap A \in Fin$
159		simpl	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap A)) \to (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin))$
160		elinel1	$⊢ y \in (x \cap A) \to y \in x$
161	160	adantl	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap A)) \to y \in x$
162	159 161 153	syl2anc	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap A)) \to F (y) \in ℝ$
163	158 162	fsumrecl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) \in ℝ$
164		infi	$⊢ x \in Fin \to x \cap B \in Fin$
165	124 164	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \in Fin$
166	165	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap B \in Fin$
167		simpl	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap B)) \to (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin))$
168		elinel1	$⊢ y \in (x \cap B) \to y \in x$
169	168	adantl	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap B)) \to y \in x$
170	167 169 153	syl2anc	$⊢ ((((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap B)) \to F (y) \in ℝ$
171	166 170	fsumrecl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} F (y) \in ℝ$
172		rexadd	$⊢ (\sum_{y \in x \cap A} F (y) \in ℝ \land \sum_{y \in x \cap B} F (y) \in ℝ) \to \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
173	163 171 172	syl2anc	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
174	173	eqcomd	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y)$
175	155 174	eqtrd	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x} F (y) = \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y)$
176		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
177	176 163	sselid	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) \in ℝ^{*}$
178	176 171	sselid	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} F (y) \in ℝ^{*}$
179	1	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to A \in V$
180	33	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
181		simpr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to \neg +∞ \in ran ({F ↾}_{A})$
182	180 181	fge0iccico	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to ({F ↾}_{A}) : A ⟶ [0, +∞)$
183	179 182	sge0reval	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) = sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <)$
184	183	eqcomd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <) = sum^({F ↾}_{A})$
185	34	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) \in ℝ^{*}$
186	184 185	eqeltrd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{}$
187	186	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{}$
188	2	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to B \in W$
189	39	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
190		simpr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in ran ({F ↾}_{B})$
191	189 190	fge0iccico	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to ({F ↾}_{B}) : B ⟶ [0, +∞)$
192	188 191	sge0reval	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{B}) = sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
193	192	eqcomd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <) = sum^({F ↾}_{B})$
194	41	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{B}) \in ℝ^{*}$
195	193 194	eqeltrd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{}$
196	195	adantlr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{}$
197	187 196	jca	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to (sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{} \land sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{})$
198	197	adantr	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to (sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{} \land sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{})$
199	177 178 198	jca31	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to ((\sum_{y \in x \cap A} F (y) \in ℝ^{} \land \sum_{y \in x \cap B} F (y) \in ℝ^{}) \land (sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{} \land sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{}))$
200	179	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to A \in V$
201	180	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
202	181	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to \neg +∞ \in ran ({F ↾}_{A})$
203	201 202	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{A}) : A ⟶ [0, +∞)$
204	99	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to x \cap A \subseteq A$
205	157	adantl	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to x \cap A \in Fin$
206	200 203 204 205	fsumlesge0	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \leq sum^({F ↾}_{A})$
207	99	sseli	$⊢ y \in (x \cap A) \to y \in A$
208		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
209	207 208	syl	$⊢ y \in (x \cap A) \to ({F ↾}_{A}) (y) = F (y)$
210	209	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap A)) \to ({F ↾}_{A}) (y) = F (y)$
211	210	sumeq2dv	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) = \sum_{y \in x \cap A} F (y)$
212	183	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to sum^({F ↾}_{A}) = sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <)$
213	211 212	breq12d	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to (\sum_{y \in x \cap A} ({F ↾}_{A}) (y) \leq sum^({F ↾}_{A}) \leftrightarrow \sum_{y \in x \cap A} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <))$
214	206 213	mpbid	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <)$
215	214	adantlr	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <)$
216	188	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to B \in W$
217	189	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
218	190	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \neg +∞ \in ran ({F ↾}_{B})$
219	217 218	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{B}) : B ⟶ [0, +∞)$
220	102	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap B \subseteq B$
221	165	adantl	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap B \in Fin$
222	216 219 220 221	fsumlesge0	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} ({F ↾}_{B}) (y) \leq sum^({F ↾}_{B})$
223	102	sseli	$⊢ y \in (x \cap B) \to y \in B$
224		fvres	$⊢ y \in B \to ({F ↾}_{B}) (y) = F (y)$
225	223 224	syl	$⊢ y \in (x \cap B) \to ({F ↾}_{B}) (y) = F (y)$
226	225	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \land y \in (x \cap B)) \to ({F ↾}_{B}) (y) = F (y)$
227	226	sumeq2dv	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} ({F ↾}_{B}) (y) = \sum_{y \in x \cap B} F (y)$
228	192	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to sum^({F ↾}_{B}) = sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
229	227 228	breq12d	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to (\sum_{y \in x \cap B} ({F ↾}_{B}) (y) \leq sum^({F ↾}_{B}) \leftrightarrow \sum_{y \in x \cap B} F (y) \leq sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <))$
230	222 229	mpbid	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} F (y) \leq sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
231	230	adantllr	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} F (y) \leq sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
232	215 231	jca	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to (\sum_{y \in x \cap A} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \land \sum_{y \in x \cap B} F (y) \leq sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <))$
233		xle2add	$⊢ ((\sum_{y \in x \cap A} F (y) \in ℝ^{} \land \sum_{y \in x \cap B} F (y) \in ℝ^{}) \land (sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{} \land sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{})) \to ((\sum_{y \in x \cap A} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \land \sum_{y \in x \cap B} F (y) \leq sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)) \to \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <))$
234	199 232 233	sylc	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap A} F (y) +_{𝑒} \sum_{y \in x \cap B} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
235	175 234	eqbrtrd	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
236	235	3adant3	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin) \land z = \sum_{y \in x} F (y)) \to \sum_{y \in x} F (y) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
237	97 236	eqbrtrd	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin) \land z = \sum_{y \in x} F (y)) \to z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
238	237	3exp	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to (x \in (𝒫 U \cap Fin) \to (z = \sum_{y \in x} F (y) \to z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)))$
239	238	rexlimdv	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to (\exists x \in (𝒫 U \cap Fin) z = \sum_{y \in x} F (y) \to z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <))$
240	239	adantr	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to (\exists x \in (𝒫 U \cap Fin) z = \sum_{y \in x} F (y) \to z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <))$
241	96 240	mpd	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
242	241	ralrimiva	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to \forall z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
243	146	sge0rnre	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
244	176	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ℝ \subseteq ℝ^{*}$
245	243 244	sstrd	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
246	187 196	xaddcld	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{*}$
247		supxrleub	$⊢ (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{} \land sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{}) \to (sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \leftrightarrow \forall z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <))$
248	245 246 247	syl2anc	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to (sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \leftrightarrow \forall z \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) z \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <))$
249	242 248	mpbird	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) \leq sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
250	14	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to U \in V$
251	250 146	sge0reval	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^(F) = sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
252	183	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{A}) = sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{*} <)$
253	192	adantlr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{B}) = sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{*} <)$
254	252 253	oveq12d	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) +_{𝑒} sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <)$
255	249 251 254	3brtr4d	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
256	91 255	pm2.61dan	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
257	69 256	pm2.61dan	$⊢ φ \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
258	257	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
259		pnfge	$⊢ sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \in ℝ^{*} \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
260	42 259	syl	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
261	260	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
262		id	$⊢ sum^(F) = +∞ \to sum^(F) = +∞$
263	262	eqcomd	$⊢ sum^(F) = +∞ \to +∞ = sum^(F)$
264	263	adantl	$⊢ (φ \land sum^(F) = +∞) \to +∞ = sum^(F)$
265	261 264	breqtrd	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq sum^(F)$
266	29 43 258 265	xrletrid	$⊢ (φ \land sum^(F) = +∞) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
267	22 27 266	syl2anc	$⊢ (φ \land \neg sum^(F) \in ℝ) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
268	21 267	pm2.61dan	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$

Metamath Proof Explorer

Theorem sge0split

Proof