Metamath Proof Explorer

Theorem 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 ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )

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 ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) ∈ ℝ* )
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 ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) = ( +∞ +e 𝐸 ) )
85 84 adantl ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = +∞ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) = ( +∞ +e 𝐸 ) )
86 53 renemnfd ⊢ ( 𝜑 → 𝐸 ≠ -∞ )
87 xaddpnf2 ⊢ ( ( 𝐸 ∈ ℝ* ∧ 𝐸 ≠ -∞ ) → ( +∞ +e 𝐸 ) = +∞ )
88 46 86 87 syl2anc ⊢ ( 𝜑 → ( +∞ +e 𝐸 ) = +∞ )
89 88 adantr ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = +∞ ) → ( +∞ +e 𝐸 ) = +∞ )
90 85 89 eqtr2d ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = +∞ ) → +∞ = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
91 83 90 breqtrd ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = +∞ ) → ( ( Σ 𝑘 ∈ 𝑈 𝐵 + Σ 𝑘 ∈ 𝑊 𝐶 ) + 𝐸 ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
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 le2addd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑈 𝐵 + Σ 𝑘 ∈ 𝑊 𝐶 ) ≤ ( Σ 𝑘 ∈ ( 𝑈 ∪ 𝑊 ) 𝐵 + Σ 𝑘 ∈ ( 𝑈 ∪ 𝑊 ) 𝐶 ) )
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 ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) + 𝐸 ) )
152 100 101 151 syl2anc ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ∈ ℝ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) + 𝐸 ) )
153 152 eqcomd ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ∈ ℝ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) + 𝐸 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
154 150 153 breqtrd ⊢ ( ( 𝜑 ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ∈ ℝ ) → ( ( Σ 𝑘 ∈ 𝑈 𝐵 + Σ 𝑘 ∈ 𝑊 𝐶 ) + 𝐸 ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
155 92 97 154 syl2anc ⊢ ( ( 𝜑 ∧ ¬ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = +∞ ) → ( ( Σ 𝑘 ∈ 𝑈 𝐵 + Σ 𝑘 ∈ 𝑊 𝐶 ) + 𝐸 ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
156 91 155 pm2.61dan ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ 𝑈 𝐵 + Σ 𝑘 ∈ 𝑊 𝐶 ) + 𝐸 ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
157 75 156 eqbrtrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ 𝑈 𝐵 + ( 𝐸 / 2 ) ) + ( Σ 𝑘 ∈ 𝑊 𝐶 + ( 𝐸 / 2 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
158 23 66 47 67 157 xrltletrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) < ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )
159 23 47 158 xrltled ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝐸 ) )