Theorem sge0split 47224

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

Hypotheses

Ref	Expression
sge0split.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sge0split.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
sge0split.u	⊢ 𝑈 = (𝐴 ∪ 𝐵)
sge0split.in0	⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
sge0split.f	⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))

Assertion

Ref	Expression
sge0split	⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))

Proof of Theorem sge0split

Dummy variables 𝑎 𝑏 𝑥 𝑧 𝑦 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0split.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2	1	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → 𝐴 ∈ 𝑉)
3		sge0split.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → 𝐵 ∈ 𝑊)
5		sge0split.u	. . . 4 ⊢ 𝑈 = (𝐴 ∪ 𝐵)
6		sge0split.in0	. . . . 5 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
7	6	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (𝐴 ∩ 𝐵) = ∅)
8		sge0split.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))
9	8	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → 𝐹:𝑈⟶(0[,]+∞))
10		simpr 490	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘𝐹) ∈ ℝ)
11	2, 4, 5, 7, 9, 10	sge0resplit 47221	. . 3 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
12		unexg 7748	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
13	1, 3, 12	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
14	5, 13	eqeltrid 2866	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ V)
15	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → 𝑈 ∈ V)
16	15, 9, 10	sge0ssre 47212	. . . . 5 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ)
17	15, 9, 10	sge0ssre 47212	. . . . 5 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ)
18		rexadd 13286	. . . . 5 ⊢ (((Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
19	16, 17, 18	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
20	19	eqcomd 2768	. . 3 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
21	11, 20	eqtrd 2797	. 2 ⊢ ((𝜑 ∧ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
22		simpl 488	. . 3 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → 𝜑)
23		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → ¬ (Σ^‘𝐹) ∈ ℝ)
24	14, 8	sge0repnf 47201	. . . . . 6 ⊢ (𝜑 → ((Σ^‘𝐹) ∈ ℝ ↔ ¬ (Σ^‘𝐹) = +∞))
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → ((Σ^‘𝐹) ∈ ℝ ↔ ¬ (Σ^‘𝐹) = +∞))
26	23, 25	mtbid 327	. . . 4 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → ¬ ¬ (Σ^‘𝐹) = +∞)
27	26	notnotrd 134	. . 3 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘𝐹) = +∞)
28	14, 8	sge0xrcl 47200	. . . . 5 ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*)
29	28	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) ∈ ℝ*)
30		ssun1 4127	. . . . . . . . . 10 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
31	30, 5	sseqtrri 3983	. . . . . . . . 9 ⊢ 𝐴 ⊆ 𝑈
32	31	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
33	8, 32	fssresd 6746	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞))
34	1, 33	sge0xrcl 47200	. . . . . 6 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ*)
35		iccssxr 13485	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ*
36		ssun2 4128	. . . . . . . . . . 11 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
37	36, 5	sseqtrri 3983	. . . . . . . . . 10 ⊢ 𝐵 ⊆ 𝑈
38	37	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
39	8, 38	fssresd 6746	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞))
40	3, 39	sge0cl 47196	. . . . . . 7 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐵)) ∈ (0[,]+∞))
41	35, 40	sselid 3932	. . . . . 6 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ*)
42	34, 41	xaddcld 13355	. . . . 5 ⊢ (𝜑 → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ∈ ℝ*)
43	42	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ∈ ℝ*)
44		pnfxr 11290	. . . . . . . . 9 ⊢ +∞ ∈ ℝ*
45		eqid 2762	. . . . . . . . 9 ⊢ +∞ = +∞
46		xreqle 46137	. . . . . . . . 9 ⊢ ((+∞ ∈ ℝ* ∧ +∞ = +∞) → +∞ ≤ +∞)
47	44, 45, 46	mp2an 705	. . . . . . . 8 ⊢ +∞ ≤ +∞
48	47	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ≤ +∞)
49	14	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝑈 ∈ V)
50	8	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝐹:𝑈⟶(0[,]+∞))
51		rnresss 6014	. . . . . . . . . . 11 ⊢ ran (𝐹 ↾ 𝐴) ⊆ ran 𝐹
52	51	sseli 3930	. . . . . . . . . 10 ⊢ (+∞ ∈ ran (𝐹 ↾ 𝐴) → +∞ ∈ ran 𝐹)
53	52	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ∈ ran 𝐹)
54	49, 50, 53	sge0pnfval 47188	. . . . . . . 8 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘𝐹) = +∞)
55		xrge0neqmnf 13507	. . . . . . . . . . . . . 14 ⊢ ((Σ^‘(𝐹 ↾ 𝐵)) ∈ (0[,]+∞) → (Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞)
56	40, 55	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞)
57		xaddpnf2 13281	. . . . . . . . . . . . 13 ⊢ (((Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ* ∧ (Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞) → (+∞ +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞)
58	41, 56, 57	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (+∞ +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞)
59	58	eqcomd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → +∞ = (+∞ +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
60	59	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ = (+∞ +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
61	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝐴 ∈ 𝑉)
62	33	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞))
63		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ∈ ran (𝐹 ↾ 𝐴))
64	61, 62, 63	sge0pnfval 47188	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘(𝐹 ↾ 𝐴)) = +∞)
65	64	oveq1d 7431	. . . . . . . . . 10 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = (+∞ +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
66	60, 54, 65	3eqtr4d 2807	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
67	66, 54	eqtr3d 2799	. . . . . . . 8 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞)
68	54, 67	breq12d 5120	. . . . . . 7 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → ((Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ↔ +∞ ≤ +∞))
69	48, 68	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
70	47	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ≤ +∞)
71	14	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝑈 ∈ V)
72	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
73		rnresss 6014	. . . . . . . . . . . . 13 ⊢ ran (𝐹 ↾ 𝐵) ⊆ ran 𝐹
74	73	sseli 3930	. . . . . . . . . . . 12 ⊢ (+∞ ∈ ran (𝐹 ↾ 𝐵) → +∞ ∈ ran 𝐹)
75	74	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ∈ ran 𝐹)
76	71, 72, 75	sge0pnfval 47188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘𝐹) = +∞)
77	3	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐵 ∈ 𝑊)
78	39	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞))
79		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ∈ ran (𝐹 ↾ 𝐵))
80	77, 78, 79	sge0pnfval 47188	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘(𝐹 ↾ 𝐵)) = +∞)
81	80	oveq2d 7432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞))
82	1, 33	sge0cl 47196	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐴)) ∈ (0[,]+∞))
83		xrge0neqmnf 13507	. . . . . . . . . . . . . 14 ⊢ ((Σ^‘(𝐹 ↾ 𝐴)) ∈ (0[,]+∞) → (Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞)
84	82, 83	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞)
85		xaddpnf1 13280	. . . . . . . . . . . . 13 ⊢ (((Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ* ∧ (Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) = +∞)
86	34, 84, 85	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) = +∞)
87	86	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) = +∞)
88	81, 87	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞)
89	76, 88	breq12d 5120	. . . . . . . . 9 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ((Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ↔ +∞ ≤ +∞))
90	70, 89	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
91	90	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
92		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
93		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
94	93	elrnmpt 5946	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
95	92, 94	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
96	95	bilani 510	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
97		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
98		inss1 4185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝑥 ∩ 𝐴)
99		inss2 4186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
100	98, 99	sstri 3943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ 𝐴
101		inss2 4186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝑥 ∩ 𝐵)
102		inss2 4186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵
103	101, 102	sstri 3943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ 𝐵
104	100, 103	ssini 4188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝐴 ∩ 𝐵)
105	104	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝐴 ∩ 𝐵))
106	105, 6	sseqtrd 3970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ ∅)
107		ss0 4355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ ∅ → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
108	106, 107	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
109	108	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
110		indi 4233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵))
111	110	eqcomi 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵))
112	111	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵)))
113	5	eqcomi 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∪ 𝐵) = 𝑈
114	113	ineq2i 4166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = (𝑥 ∩ 𝑈)
115	114	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ (𝐴 ∪ 𝐵)) = (𝑥 ∩ 𝑈))
116		elinel1 4150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
117		elpwi 4567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈)
118	116, 117	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ⊆ 𝑈)
119		dfss2 3920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ 𝑈 ↔ (𝑥 ∩ 𝑈) = 𝑥)
120	119	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ 𝑈 → (𝑥 ∩ 𝑈) = 𝑥)
121	118, 120	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝑈) = 𝑥)
122	112, 115, 121	3eqtrrd 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)))
123	122	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)))
124		elinel2 4151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
125	124	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
126		rge0ssre 13511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0[,)+∞) ⊆ ℝ
127	8	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
128		pm4.56 1004	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ +∞ ∈ ran (𝐹 ↾ 𝐴) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ↔ ¬ (+∞ ∈ ran (𝐹 ↾ 𝐴) ∨ +∞ ∈ ran (𝐹 ↾ 𝐵)))
129	128	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((¬ +∞ ∈ ran (𝐹 ↾ 𝐴) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ¬ (+∞ ∈ ran (𝐹 ↾ 𝐴) ∨ +∞ ∈ ran (𝐹 ↾ 𝐵)))
130		elun 4103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (+∞ ∈ (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) ↔ (+∞ ∈ ran (𝐹 ↾ 𝐴) ∨ +∞ ∈ ran (𝐹 ↾ 𝐵)))
131	129, 130	sylnibr 332	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ +∞ ∈ ran (𝐹 ↾ 𝐴) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈ (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)))
132	131	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈ (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)))
133		rnresun 45999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵))
134	133	eqcomi 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran (𝐹 ↾ (𝐴 ∪ 𝐵))
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran (𝐹 ↾ (𝐴 ∪ 𝐵)))
136	113	reseq2i 5973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 ↾ (𝐴 ∪ 𝐵)) = (𝐹 ↾ 𝑈)
137	136	rneqi 5925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = ran (𝐹 ↾ 𝑈)
138	137	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = ran (𝐹 ↾ 𝑈))
139		ffn 6706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹:𝑈⟶(0[,]+∞) → 𝐹 Fn 𝑈)
140		fnresdm 6655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 Fn 𝑈 → (𝐹 ↾ 𝑈) = 𝐹)
141	8, 139, 140	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐹 ↾ 𝑈) = 𝐹)
142	141	rneqd 5926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ran (𝐹 ↾ 𝑈) = ran 𝐹)
143	135, 138, 142	3eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran 𝐹)
144	143	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran 𝐹)
145	132, 144	neleqtrd 2884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈ ran 𝐹)
146	127, 145	fge0iccico 47185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,)+∞))
147	146	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑈⟶(0[,)+∞))
148	118	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑈)
149		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
150	148, 149	sseldd 3935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈)
151	150	adantll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈)
152	147, 151	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞))
153	126, 152	sselid 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ)
154	153	recnd 11264	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ)
155	109, 123, 125, 154	fsumsplit 15829	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
156		infi 9243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ Fin → (𝑥 ∩ 𝐴) ∈ Fin)
157	124, 156	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ∈ Fin)
158	157	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ∈ Fin)
159		simpl 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
160		elinel1 4150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → 𝑦 ∈ 𝑥)
161	160	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → 𝑦 ∈ 𝑥)
162	159, 161, 153	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → (𝐹‘𝑦) ∈ ℝ)
163	158, 162	fsumrecl 15822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ)
164		infi 9243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ Fin → (𝑥 ∩ 𝐵) ∈ Fin)
165	124, 164	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐵) ∈ Fin)
166	165	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin)
167		simpl 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
168		elinel1 4150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → 𝑦 ∈ 𝑥)
169	168	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → 𝑦 ∈ 𝑥)
170	167, 169, 153	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → (𝐹‘𝑦) ∈ ℝ)
171	166, 170	fsumrecl 15822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ)
172		rexadd 13286	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
173	163, 171, 172	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
174	173	eqcomd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
175	155, 174	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
176		ressxr 11280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℝ ⊆ ℝ*
177	176, 163	sselid 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ*)
178	176, 171	sselid 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ*)
179	1	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝐴 ∈ 𝑉)
180	33	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞))
181		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → ¬ +∞ ∈ ran (𝐹 ↾ 𝐴))
182	180, 181	fge0iccico 47185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,)+∞))
183	179, 182	sge0reval 47187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ))
184	183	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) = (Σ^‘(𝐹 ↾ 𝐴)))
185	34	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ*)
186	184, 185	eqeltrd 2862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
187	186	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
188	3	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐵 ∈ 𝑊)
189	39	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞))
190		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈ ran (𝐹 ↾ 𝐵))
191	189, 190	fge0iccico 47185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,)+∞))
192	188, 191	sge0reval 47187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))
193	192	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) = (Σ^‘(𝐹 ↾ 𝐵)))
194	41	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ*)
195	193, 194	eqeltrd 2862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
196	195	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
197	187, 196	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
198	197	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
199	177, 178, 198	jca31 524	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ* ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ*) ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)))
200	179	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐴 ∈ 𝑉)
201	180	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞))
202	181	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹 ↾ 𝐴))
203	201, 202	fge0iccico 47185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,)+∞))
204	99	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ⊆ 𝐴)
205	157	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ∈ Fin)
206	200, 203, 204, 205	fsumlesge0 47192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ≤ (Σ^‘(𝐹 ↾ 𝐴)))
207	99	sseli 3930	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → 𝑦 ∈ 𝐴)
208		fvres 6901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
209	207, 208	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
210	209	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
211	210	sumeq2dv 15791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦))
212	183	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ))
213	211, 212	breq12d 5120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ≤ (Σ^‘(𝐹 ↾ 𝐴)) ↔ Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )))
214	206, 213	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ))
215	214	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ))
216	188	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐵 ∈ 𝑊)
217	189	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞))
218	190	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹 ↾ 𝐵))
219	217, 218	fge0iccico 47185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,)+∞))
220	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ⊆ 𝐵)
221	165	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin)
222	216, 219, 220, 221	fsumlesge0 47192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) ≤ (Σ^‘(𝐹 ↾ 𝐵)))
223	102	sseli 3930	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → 𝑦 ∈ 𝐵)
224		fvres 6901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦))
225	223, 224	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦))
226	225	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦))
227	226	sumeq2dv 15791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))
228	192	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))
229	227, 228	breq12d 5120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) ≤ (Σ^‘(𝐹 ↾ 𝐵)) ↔ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
230	222, 229	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))
231	230	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))
232	215, 231	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
233		xle2add 13313	. . . . . . . . . . . . . . . . . 18 ⊢ (((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ* ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ*) ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)) → ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))))
234	199, 232, 233	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
235	175, 234	eqbrtrd 5131	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
236	235	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
237	97, 236	eqbrtrd 5131	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
238	237	3exp 1137	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))))
239	238	rexlimdv 3163	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))))
240	239	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))))
241	96, 240	mpd 16	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
242	241	ralrimiva 3156	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
243	146	sge0rnre 47179	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ)
244	176	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ℝ ⊆ ℝ*)
245	243, 244	sstrd 3944	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ*)
246	187, 196	xaddcld 13355	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ∈ ℝ*)
247		supxrleub 13380	. . . . . . . . . 10 ⊢ ((ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ∈ ℝ*) → (sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))))
248	245, 246, 247	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))))
249	242, 248	mpbird 260	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
250	14	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝑈 ∈ V)
251	250, 146	sge0reval 47187	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ))
252	183	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ))
253	192	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ))
254	252, 253	oveq12d 7434	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )))
255	249, 251, 254	3brtr4d 5141	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
256	91, 255	pm2.61dan 825	. . . . . 6 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
257	69, 256	pm2.61dan 825	. . . . 5 ⊢ (𝜑 → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
258	257	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) ≤ ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
259		pnfge 13183	. . . . . . 7 ⊢ (((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ∈ ℝ* → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞)
260	42, 259	syl 18	. . . . . 6 ⊢ (𝜑 → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞)
261	260	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞)
262		id 23	. . . . . . 7 ⊢ ((Σ^‘𝐹) = +∞ → (Σ^‘𝐹) = +∞)
263	262	eqcomd 2768	. . . . . 6 ⊢ ((Σ^‘𝐹) = +∞ → +∞ = (Σ^‘𝐹))
264	263	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → +∞ = (Σ^‘𝐹))
265	261, 264	breqtrd 5135	. . . 4 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))) ≤ (Σ^‘𝐹))
266	29, 43, 258, 265	xrletrid 13208	. . 3 ⊢ ((𝜑 ∧ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
267	22, 27, 266	syl2anc 596	. 2 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) ∈ ℝ) → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
268	21, 267	pm2.61dan 825	1 ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560   class class class wbr 5107   ↦ cmpt 5190  ran crn 5660   ↾ cres 5661   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  Fincfn 8955  supcsup 9413  ℝcr 11126  0cc0 11127   + caddc 11130  +∞cpnf 11267  -∞cmnf 11268  ℝ^*cxr 11269   < clt 11270   ≤ cle 11271   +_𝑒 cxad 13163  [,)cico 13402  [,]cicc 13403  Σcsu 15775  Σ^{^}csumge0 47177

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9415  df-oi 9485  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-n0 12532  df-z 12619  df-uz 12891  df-rp 13045  df-xadd 13166  df-ico 13406  df-icc 13407  df-fz 13564  df-fzo 13712  df-seq 14068  df-exp 14128  df-hash 14397  df-cj 15188  df-re 15189  df-im 15190  df-sqrt 15324  df-abs 15325  df-clim 15577  df-sum 15776  df-sumge0 47178

This theorem is used by:  sge0splitmpt  47226