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		simpr	$⊢ (((φ \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 \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
93		vex	$⊢ z \in V$
94		eqid	$⊢ (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
95	94	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))$
96	93 95	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)$
97	92 96	sylib	$⊢ (((φ \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)$
98		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)$
99		inss1	$⊢ (x \cap A) \cap (x \cap B) \subseteq x \cap A$
100		inss2	$⊢ x \cap A \subseteq A$
101	99 100	sstri	$⊢ (x \cap A) \cap (x \cap B) \subseteq A$
102		inss2	$⊢ (x \cap A) \cap (x \cap B) \subseteq x \cap B$
103		inss2	$⊢ x \cap B \subseteq B$
104	102 103	sstri	$⊢ (x \cap A) \cap (x \cap B) \subseteq B$
105	101 104	ssini	$⊢ (x \cap A) \cap (x \cap B) \subseteq A \cap B$
106	105	a1i	$⊢ φ \to (x \cap A) \cap (x \cap B) \subseteq A \cap B$
107	106 4	sseqtrd	$⊢ φ \to (x \cap A) \cap (x \cap B) \subseteq \emptyset$
108		ss0	$⊢ (x \cap A) \cap (x \cap B) \subseteq \emptyset \to (x \cap A) \cap (x \cap B) = \emptyset$
109	107 108	syl	$⊢ φ \to (x \cap A) \cap (x \cap B) = \emptyset$
110	109	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$
111		indi	$⊢ x \cap (A \cup B) = (x \cap A) \cup (x \cap B)$
112	111	eqcomi	$⊢ (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
113	112	a1i	$⊢ x \in (𝒫 U \cap Fin) \to (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
114	3	eqcomi	$⊢ A \cup B = U$
115	114	ineq2i	$⊢ x \cap (A \cup B) = x \cap U$
116	115	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap (A \cup B) = x \cap U$
117		elinel1	$⊢ x \in (𝒫 U \cap Fin) \to x \in 𝒫 U$
118		elpwi	$⊢ x \in 𝒫 U \to x \subseteq U$
119	117 118	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \subseteq U$
120		dfss2	$⊢ x \subseteq U \leftrightarrow x \cap U = x$
121	120	biimpi	$⊢ x \subseteq U \to x \cap U = x$
122	119 121	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap U = x$
123	113 116 122	3eqtrrd	$⊢ x \in (𝒫 U \cap Fin) \to x = (x \cap A) \cup (x \cap B)$
124	123	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)$
125		elinel2	$⊢ x \in (𝒫 U \cap Fin) \to x \in Fin$
126	125	adantl	$⊢ (((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \in Fin$
127		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
128	5	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to F : U ⟶ [0, +∞]$
129		pm4.56	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \leftrightarrow \neg (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
130	129	biimpi	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
131		elun	$⊢ +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B})) \leftrightarrow (+∞ \in ran ({F ↾}_{A}) \lor +∞ \in ran ({F ↾}_{B}))$
132	130 131	sylnibr	$⊢ (\neg +∞ \in ran ({F ↾}_{A}) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}))$
133	132	adantll	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in (ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}))$
134		rnresun	$⊢ ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{A}) \cup ran ({F ↾}_{B})$
135	134	eqcomi	$⊢ ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran ({F ↾}_{(A \cup B)})$
136	135	a1i	$⊢ φ \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran ({F ↾}_{(A \cup B)})$
137	114	reseq2i	$⊢ {F ↾}_{(A \cup B)} = {F ↾}_{U}$
138	137	rneqi	$⊢ ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{U})$
139	138	a1i	$⊢ φ \to ran ({F ↾}_{(A \cup B)}) = ran ({F ↾}_{U})$
140		ffn	$⊢ F : U ⟶ [0, +∞] \to F Fn U$
141		fnresdm	$⊢ F Fn U \to {F ↾}_{U} = F$
142	5 140 141	3syl	$⊢ φ \to {F ↾}_{U} = F$
143	142	rneqd	$⊢ φ \to ran ({F ↾}_{U}) = ran F$
144	136 139 143	3eqtrd	$⊢ φ \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran F$
145	144	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ran ({F ↾}_{A}) \cup ran ({F ↾}_{B}) = ran F$
146	133 145	neleqtrd	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in ran F$
147	128 146	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to F : U ⟶ [0, +∞)$
148	147	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, +∞)$
149	119	adantr	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to x \subseteq U$
150		simpr	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in x$
151	149 150	sseldd	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in U$
152	151	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$
153	148 152	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, +∞)$
154	127 153	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 ℝ$
155	154	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 ℂ$
156	110 124 126 155	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)$
157		infi	$⊢ x \in Fin \to x \cap A \in Fin$
158	125 157	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in Fin$
159	158	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$
160		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))$
161		elinel1	$⊢ y \in (x \cap A) \to y \in x$
162	161	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$
163	160 162 154	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 ℝ$
164	159 163	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 ℝ$
165		infi	$⊢ x \in Fin \to x \cap B \in Fin$
166	125 165	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \in Fin$
167	166	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$
168		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))$
169		elinel1	$⊢ y \in (x \cap B) \to y \in x$
170	169	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$
171	168 170 154	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 ℝ$
172	167 171	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 ℝ$
173		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)$
174	164 172 173	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)$
175	174	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)$
176	156 175	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)$
177		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
178	177 164	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 ℝ^{*}$
179	177 172	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 ℝ^{*}$
180	1	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to A \in V$
181	33	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
182		simpr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to \neg +∞ \in ran ({F ↾}_{A})$
183	181 182	fge0iccico	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to ({F ↾}_{A}) : A ⟶ [0, +∞)$
184	180 183	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)) ℝ^{*} <)$
185	184	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})$
186	34	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sum^({F ↾}_{A}) \in ℝ^{*}$
187	185 186	eqeltrd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \sum_{b \in a} ({F ↾}_{A}) (b)) ℝ^{} <) \in ℝ^{}$
188	187	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 ℝ^{}$
189	2	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to B \in W$
190	39	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
191		simpr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to \neg +∞ \in ran ({F ↾}_{B})$
192	190 191	fge0iccico	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to ({F ↾}_{B}) : B ⟶ [0, +∞)$
193	189 192	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)) ℝ^{*} <)$
194	193	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})$
195	41	adantr	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^({F ↾}_{B}) \in ℝ^{*}$
196	194 195	eqeltrd	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{B})) \to sup (ran (c \in (𝒫 B \cap Fin) ⟼ \sum_{d \in c} ({F ↾}_{B}) (d)) ℝ^{} <) \in ℝ^{}$
197	196	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 ℝ^{}$
198	188 197	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 ℝ^{})$
199	198	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 ℝ^{})$
200	178 179 199	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 ℝ^{}))$
201	180	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to A \in V$
202	181	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
203	182	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to \neg +∞ \in ran ({F ↾}_{A})$
204	202 203	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{A}) : A ⟶ [0, +∞)$
205	100	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to x \cap A \subseteq A$
206	158	adantl	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land x \in (𝒫 U \cap Fin)) \to x \cap A \in Fin$
207	201 204 205 206	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})$
208	100	sseli	$⊢ y \in (x \cap A) \to y \in A$
209		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
210	208 209	syl	$⊢ y \in (x \cap A) \to ({F ↾}_{A}) (y) = F (y)$
211	210	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)$
212	211	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)$
213	184	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)) ℝ^{*} <)$
214	212 213	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)) ℝ^{*} <))$
215	207 214	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)) ℝ^{*} <)$
216	215	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)) ℝ^{*} <)$
217	189	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to B \in W$
218	190	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
219	191	adantr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to \neg +∞ \in ran ({F ↾}_{B})$
220	218 219	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to ({F ↾}_{B}) : B ⟶ [0, +∞)$
221	103	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap B \subseteq B$
222	166	adantl	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{B})) \land x \in (𝒫 U \cap Fin)) \to x \cap B \in Fin$
223	217 220 221 222	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})$
224	103	sseli	$⊢ y \in (x \cap B) \to y \in B$
225		fvres	$⊢ y \in B \to ({F ↾}_{B}) (y) = F (y)$
226	224 225	syl	$⊢ y \in (x \cap B) \to ({F ↾}_{B}) (y) = F (y)$
227	226	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)$
228	227	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)$
229	193	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)) ℝ^{*} <)$
230	228 229	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)) ℝ^{*} <))$
231	223 230	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)) ℝ^{*} <)$
232	231	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)) ℝ^{*} <)$
233	216 232	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)) ℝ^{} <))$
234		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)) ℝ^{} <))$
235	200 233 234	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)) ℝ^{} <)$
236	176 235	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)) ℝ^{} <)$
237	236	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)) ℝ^{} <)$
238	98 237	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)) ℝ^{} <)$
239	238	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)) ℝ^{} <)))$
240	239	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)) ℝ^{} <))$
241	240	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)) ℝ^{} <))$
242	97 241	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)) ℝ^{} <)$
243	242	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)) ℝ^{} <)$
244	147	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 ℝ$
245	177	a1i	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to ℝ \subseteq ℝ^{*}$
246	244 245	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 ℝ^{*}$
247	188 197	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 ℝ^{*}$
248		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)) ℝ^{*} <))$
249	246 247 248	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)) ℝ^{*} <))$
250	243 249	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)) ℝ^{*} <)$
251	14	ad2antrr	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to U \in V$
252	251 147	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)) ℝ^{*} <)$
253	184	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)) ℝ^{*} <)$
254	193	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)) ℝ^{*} <)$
255	253 254	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)) ℝ^{} <)$
256	250 252 255	3brtr4d	$⊢ ((φ \land \neg +∞ \in ran ({F ↾}_{A})) \land \neg +∞ \in ran ({F ↾}_{B})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
257	91 256	pm2.61dan	$⊢ (φ \land \neg +∞ \in ran ({F ↾}_{A})) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
258	69 257	pm2.61dan	$⊢ φ \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
259	258	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^(F) \leq sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
260		pnfge	$⊢ sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \in ℝ^{*} \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
261	42 260	syl	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
262	261	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq +∞$
263		id	$⊢ sum^(F) = +∞ \to sum^(F) = +∞$
264	263	eqcomd	$⊢ sum^(F) = +∞ \to +∞ = sum^(F)$
265	264	adantl	$⊢ (φ \land sum^(F) = +∞) \to +∞ = sum^(F)$
266	262 265	breqtrd	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) \leq sum^(F)$
267	29 43 259 266	xrletrid	$⊢ (φ \land sum^(F) = +∞) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
268	22 27 267	syl2anc	$⊢ (φ \land \neg sum^(F) \in ℝ) \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
269	21 268	pm2.61dan	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$

Metamath Proof Explorer

Theorem sge0split

Proof