Theorem sge0xaddlem1 46418

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

Hypotheses

Ref	Expression
sge0xaddlem1.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sge0xaddlem1.b	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
sge0xaddlem1.c	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞))
sge0xaddlem1.rp	⊢ (𝜑 → 𝐸 ∈ ℝ+)
sge0xaddlem1.u	⊢ (𝜑 → 𝑈 ⊆ 𝐴)
sge0xaddlem1.ufi	⊢ (𝜑 → 𝑈 ∈ Fin)
sge0xaddlem1.7	⊢ (𝜑 → 𝑊 ⊆ 𝐴)
sge0xaddlem1.wfi	⊢ (𝜑 → 𝑊 ∈ Fin)
sge0xaddlem1.ltb	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) < (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)))
sge0xaddlem1.ltc	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) < (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2)))
sge0xaddlem1.xr	⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ (0[,]+∞))
sge0xaddlem1.sb	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)
sge0xaddlem1.sc	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ)

Assertion

Ref	Expression
sge0xaddlem1	⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))

Distinct variable groups:   𝐴,𝑘,𝑥   𝑥,𝐵   𝑥,𝐶   𝑈,𝑘,𝑥   𝑘,𝑊,𝑥   𝜑,𝑘,𝑥

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)   𝐸(𝑥,𝑘)   𝑉(𝑥,𝑘)

Proof of Theorem sge0xaddlem1

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1914	. . . . 5 ⊢ Ⅎ𝑘𝜑
2		sge0xaddlem1.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		sge0xaddlem1.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
4	1, 2, 3	sge0revalmpt 46363	. . . 4 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ))
5		sge0xaddlem1.c	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞))
6	1, 2, 5	sge0revalmpt 46363	. . . 4 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < ))
7	4, 6	oveq12d 7367	. . 3 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) = (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < )))
8	4	eqcomd 2735	. . . . . 6 ⊢ (𝜑 → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
9		sge0xaddlem1.sb	. . . . . 6 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)
10	8, 9	eqeltrd 2828	. . . . 5 ⊢ (𝜑 → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) ∈ ℝ)
11		sge0xaddlem1.sc	. . . . . 6 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ)
12	6, 11	eqeltrrd 2829	. . . . 5 ⊢ (𝜑 → sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < ) ∈ ℝ)
13	10, 12	readdcld 11144	. . . 4 ⊢ (𝜑 → (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < )) ∈ ℝ)
14	13	rexrd 11165	. . 3 ⊢ (𝜑 → (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < )) ∈ ℝ*)
15	7, 14	eqeltrd 2828	. 2 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ∈ ℝ*)
16		elinel2 4153	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin)
17	16	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin)
18		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝜑)
19		elpwinss 45031	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ 𝐴)
21		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥)
22	20, 21	sseldd 3936	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴)
23	22	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴)
24		rge0ssre 13359	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
25	24, 3	sselid 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
26	18, 23, 25	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ ℝ)
27	24, 5	sselid 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)
28	18, 23, 27	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐶 ∈ ℝ)
29	26, 28	readdcld 11144	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → (𝐵 + 𝐶) ∈ ℝ)
30	17, 29	fsumrecl 15641	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ)
31	30	rexrd 11165	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ*)
32	31	ralrimiva 3121	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ*)
33		eqid 2729	. . . . . 6 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))
34	33	rnmptss 7057	. . . . 5 ⊢ (∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ* → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ*)
35	32, 34	syl 17	. . . 4 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ*)
36		supxrcl 13217	. . . 4 ⊢ (ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ* → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ*)
37	35, 36	syl 17	. . 3 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ*)
38		sge0xaddlem1.rp	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ+)
39	38	rpxrd 12938	. . 3 ⊢ (𝜑 → 𝐸 ∈ ℝ*)
40	37, 39	xaddcld 13203	. 2 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸) ∈ ℝ*)
41		sge0xaddlem1.ufi	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ Fin)
42		simpl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝜑)
43		sge0xaddlem1.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ⊆ 𝐴)
44	43	sselda 3935	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐴)
45	42, 44, 3	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐵 ∈ (0[,)+∞))
46	24, 45	sselid 3933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐵 ∈ ℝ)
47	41, 46	fsumrecl 15641	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ∈ ℝ)
48	38	rpred 12937	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ)
49	48	rehalfcld 12371	. . . . . 6 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
50	47, 49	readdcld 11144	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) ∈ ℝ)
51		sge0xaddlem1.wfi	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Fin)
52	24	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (0[,)+∞) ⊆ ℝ)
53		simpl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝜑)
54		sge0xaddlem1.7	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ 𝐴)
55	54	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑊 ⊆ 𝐴)
56		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊)
57	55, 56	sseldd 3936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝐴)
58	53, 57, 5	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐶 ∈ (0[,)+∞))
59	52, 58	sseldd 3936	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐶 ∈ ℝ)
60	51, 59	fsumrecl 15641	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ∈ ℝ)
61	60, 49	readdcld 11144	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2)) ∈ ℝ)
62	50, 61	readdcld 11144	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ∈ ℝ)
63	62	rexrd 11165	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ∈ ℝ*)
64		sge0xaddlem1.ltb	. . . 4 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) < (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)))
65		sge0xaddlem1.ltc	. . . 4 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) < (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2)))
66	9, 11, 50, 61, 64, 65	ltadd12dd 45327	. . 3 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) < ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))))
67	47	recnd 11143	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ∈ ℂ)
68	49	recnd 11143	. . . . . 6 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
69	60	recnd 11143	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ∈ ℂ)
70	67, 68, 69, 68	add4d 11345	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + ((𝐸 / 2) + (𝐸 / 2))))
71	48	recnd 11143	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
72	71	2halvesd 12370	. . . . . 6 ⊢ (𝜑 → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
73	72	oveq2d 7365	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + ((𝐸 / 2) + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸))
74	70, 73	eqtrd 2764	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸))
75	74, 63	eqeltrrd 2829	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈ ℝ*)
76		pnfxr 11169	. . . . . . . . 9 ⊢ +∞ ∈ ℝ*
77	76	a1i 11	. . . . . . . 8 ⊢ (𝜑 → +∞ ∈ ℝ*)
78	74, 62	eqeltrrd 2829	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈ ℝ)
79		ltpnf 13022	. . . . . . . . 9 ⊢ (((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈ ℝ → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) < +∞)
80	78, 79	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) < +∞)
81	75, 77, 80	xrltled 13052	. . . . . . 7 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ +∞)
82	81	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ +∞)
83		oveq1 7356	. . . . . . . 8 ⊢ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞ → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸) = (+∞ +𝑒 𝐸))
84	83	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸) = (+∞ +𝑒 𝐸))
85	48	renemnfd 11167	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ≠ -∞)
86		xaddpnf2 13129	. . . . . . . . 9 ⊢ ((𝐸 ∈ ℝ* ∧ 𝐸 ≠ -∞) → (+∞ +𝑒 𝐸) = +∞)
87	39, 85, 86	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (+∞ +𝑒 𝐸) = +∞)
88	87	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → (+∞ +𝑒 𝐸) = +∞)
89	84, 88	eqtr2d 2765	. . . . . 6 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → +∞ = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
90	82, 89	breqtrd 5118	. . . . 5 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
91		simpl 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → 𝜑)
92		sge0xaddlem1.xr	. . . . . . . 8 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ (0[,]+∞))
93	91, 92	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ (0[,]+∞))
94		neqne 2933	. . . . . . . 8 ⊢ (¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠ +∞)
95	94	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠ +∞)
96		ge0xrre 45516	. . . . . . 7 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ (0[,]+∞) ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠ +∞) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ)
97	93, 95, 96	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ)
98	47, 60	readdcld 11144	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ∈ ℝ)
99	98	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ∈ ℝ)
100		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ)
101	48	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → 𝐸 ∈ ℝ)
102	41, 51	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 ∈ Fin ∧ 𝑊 ∈ Fin))
103		unfi 9085	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ Fin ∧ 𝑊 ∈ Fin) → (𝑈 ∪ 𝑊) ∈ Fin)
104	102, 103	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ Fin)
105		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝜑)
106	43, 54	unssd 4143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 ∪ 𝑊) ⊆ 𝐴)
107	106	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → (𝑈 ∪ 𝑊) ⊆ 𝐴)
108		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝑘 ∈ (𝑈 ∪ 𝑊))
109	107, 108	sseldd 3936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝑘 ∈ 𝐴)
110	105, 109, 25	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐵 ∈ ℝ)
111	109, 27	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐶 ∈ ℝ)
112	110, 111	readdcld 11144	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → (𝐵 + 𝐶) ∈ ℝ)
113	104, 112	fsumrecl 15641	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ℝ)
114	113	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ℝ)
115	104, 110	fsumrecl 15641	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 ∈ ℝ)
116	104, 111	fsumrecl 15641	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶 ∈ ℝ)
117		icossicc 13339	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
118	117, 3	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
119		xrge0ge0 45331	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ (0[,]+∞) → 0 ≤ 𝐵)
120	118, 119	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)
121	109, 120	syldan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 0 ≤ 𝐵)
122		ssun1 4129	. . . . . . . . . . . . . 14 ⊢ 𝑈 ⊆ (𝑈 ∪ 𝑊)
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ⊆ (𝑈 ∪ 𝑊))
124	104, 110, 121, 123	fsumless 15703	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵)
125	117, 5	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))
126		xrge0ge0 45331	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ (0[,]+∞) → 0 ≤ 𝐶)
127	125, 126	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐶)
128	109, 127	syldan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 0 ≤ 𝐶)
129		ssun2 4130	. . . . . . . . . . . . . 14 ⊢ 𝑊 ⊆ (𝑈 ∪ 𝑊)
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ⊆ (𝑈 ∪ 𝑊))
131	104, 111, 128, 130	fsumless 15703	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶)
132	47, 60, 115, 116, 124, 131	le2addd 11739	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶))
133	110	recnd 11143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐵 ∈ ℂ)
134	111	recnd 11143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐶 ∈ ℂ)
135	104, 133, 134	fsumadd 15647	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) = (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶))
136	135	eqcomd 2735	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶) = Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶))
137	132, 136	breqtrd 5118	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶))
138	137	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶))
139	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ*)
140	104, 106	elpwd 4557	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ 𝒫 𝐴)
141	140, 104	elind 4151	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ (𝒫 𝐴 ∩ Fin))
142	113	elexd 3460	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ V)
143		sumeq1 15596	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑈 ∪ 𝑊) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) = Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶))
144	33, 143	elrnmpt1s 5901	. . . . . . . . . . . 12 ⊢ (((𝑈 ∪ 𝑊) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ V) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)))
145	141, 142, 144	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)))
146	145	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)))
147		supxrub 13226	. . . . . . . . . 10 ⊢ ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ* ∧ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ))
148	139, 146, 147	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ))
149	99, 114, 100, 138, 148	letrd 11273	. . . . . . . 8 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ))
150	99, 100, 101, 149	leadd1dd 11734	. . . . . . 7 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸))
151		rexadd 13134	. . . . . . . . 9 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸))
152	100, 101, 151	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸))
153	152	eqcomd 2735	. . . . . . 7 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
154	150, 153	breqtrd 5118	. . . . . 6 ⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ ℝ) → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
155	91, 97, 154	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞) → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
156	90, 155	pm2.61dan 812	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
157	74, 156	eqbrtrd 5114	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
158	15, 63, 40, 66, 157	xrltletrd 13063	. 2 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) < (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))
159	15, 40, 158	xrltled 13052	1 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3436   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  𝒫 cpw 4551   class class class wbr 5092   ↦ cmpt 5173  ran crn 5620  ‘cfv 6482  (class class class)co 7349  Fincfn 8872  supcsup 9330  ℝcr 11008  0cc0 11009   + caddc 11012  +∞cpnf 11146  -∞cmnf 11147  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150   / cdiv 11777  2c2 12183  ℝ⁺crp 12893   +_𝑒 cxad 13012  [,)cico 13250  [,]cicc 13251  Σcsu 15593  Σ^{^}csumge0 46347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-rp 12894  df-xadd 13015  df-ico 13254  df-icc 13255  df-fz 13411  df-fzo 13558  df-seq 13909  df-exp 13969  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-sum 15594  df-sumge0 46348

This theorem is referenced by:  sge0xaddlem2  46419