sge0xaddlem1

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

	Ref	Expression
Hypotheses	sge0xaddlem1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	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	sge0xaddlem1	⊢ ( 𝜑 → ( ( Σ^{^} ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^{^} ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ^* , < ) +_𝑒 𝐸 ) )

Proof

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

Metamath Proof Explorer

Theorem sge0xaddlem1

Proof