Metamath Proof Explorer

Theorem sge0xaddlem2

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

Ref Expression
Hypotheses sge0xaddlem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0xaddlem2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
sge0xaddlem2.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
sge0xaddlem2.sb ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
sge0xaddlem2.sc ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ )
Assertion sge0xaddlem2 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0xaddlem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0xaddlem2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3 sge0xaddlem2.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
4 sge0xaddlem2.sb ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
5 sge0xaddlem2.sc ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ )
6 nfv ⊢ Ⅎ 𝑘 𝜑
7 0xr ⊢ 0 ∈ ℝ*
8 7 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ℝ* )
9 pnfxr ⊢ +∞ ∈ ℝ*
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → +∞ ∈ ℝ* )
11 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
12 11 2 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
13 11 3 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
14 12 13 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
15 14 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ* )
16 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
17 16 2 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
18 xrge0ge0 ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝐵 )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
20 16 3 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
21 xrge0ge0 ⊢ ( 𝐶 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝐶 )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐶 )
23 12 13 19 22 addge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( 𝐵 + 𝐶 ) )
24 14 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) < +∞ )
25 8 10 15 23 24 elicod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ( 0 [,) +∞ ) )
26 6 1 25 sge0revalmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
27 rexadd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +e 𝐶 ) = ( 𝐵 + 𝐶 ) )
28 12 13 27 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +e 𝐶 ) = ( 𝐵 + 𝐶 ) )
29 28 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
31 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
32 4 5 31 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
33 6 1 2 sge0revalmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) )
34 6 1 3 sge0revalmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) )
35 33 34 oveq12d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
36 33 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
37 36 4 eqeltrd ⊢ ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) ∈ ℝ )
38 34 5 eqeltrrd ⊢ ( 𝜑 → sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ∈ ℝ )
39 37 38 readdcld ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ∈ ℝ )
40 39 rexrd ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ∈ ℝ* )
41 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
43 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝜑 )
44 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
45 44 adantr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ⊆ 𝐴 )
46 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑥 )
47 45 46 sseldd ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐴 )
48 47 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐴 )
49 43 48 12 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
50 43 48 13 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐶 ∈ ℝ )
51 49 50 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
52 42 51 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ∈ ℝ )
53 52 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ∈ ℝ* )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ∈ ℝ* )
55 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) )
56 55 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) ⊆ ℝ* )
57 54 56 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) ⊆ ℝ* )
58 supxrcl ⊢ ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) ⊆ ℝ* → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ∈ ℝ* )
59 57 58 syl ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ∈ ℝ* )
60 35 eqcomd ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
62 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑒 ∈ ℝ+ )
63 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝐴 ∈ 𝑉 )
64 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
65 rphalfcl ⊢ ( 𝑒 ∈ ℝ+ → ( 𝑒 / 2 ) ∈ ℝ+ )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 / 2 ) ∈ ℝ+ )
67 4 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
68 62 63 64 66 67 sge0ltfirpmpt2 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) )
69 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
70 5 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ )
71 62 63 69 66 70 sge0ltfirpmpt2 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) )
72 71 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) )
73 63 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → 𝐴 ∈ 𝑉 )
74 73 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝐴 ∈ 𝑉 )
75 simpl1l ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → 𝜑 )
76 75 3ad2antl1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → 𝜑 )
77 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
78 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
79 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
80 79 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ )
81 78 80 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
82 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
83 82 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
84 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
85 84 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) )
86 83 85 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) ) )
87 81 86 2 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
88 76 77 87 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
89 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
90 89 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ )
91 78 90 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ ) )
92 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
93 92 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ ) ) )
94 83 93 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ ) ) ) )
95 91 94 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ ) )
96 76 77 95 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,) +∞ ) )
97 simp11r ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑒 ∈ ℝ+ )
98 simp12 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) )
99 elpwinss ⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ⊆ 𝐴 )
100 98 99 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑢 ⊆ 𝐴 )
101 elinel2 ⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ∈ Fin )
102 101 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → 𝑢 ∈ Fin )
103 102 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑢 ∈ Fin )
104 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) )
105 elpwinss ⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ⊆ 𝐴 )
106 104 105 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑣 ⊆ 𝐴 )
107 elinel2 ⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ∈ Fin )
108 107 3ad2ant2 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝑣 ∈ Fin )
109 simp13 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) )
110 nfcv ⊢ Ⅎ 𝑗 𝐵
111 110 79 84 cbvmpt ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
112 111 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
113 84 110 79 cbvsum ⊢ Σ 𝑘 ∈ 𝑢 𝐵 = Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
114 113 oveq1i ⊢ ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) = ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) )
115 112 114 breq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
116 115 biimpi ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
117 109 116 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
118 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) )
119 nfcv ⊢ Ⅎ 𝑗 𝐶
120 119 89 92 cbvmpt ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
121 120 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
122 92 119 89 cbvsum ⊢ Σ 𝑘 ∈ 𝑣 𝐶 = Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
123 122 oveq1i ⊢ ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) = ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) )
124 121 123 breq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
125 124 biimpi ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
126 118 125 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
127 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝜑 )
128 84 92 oveq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 + 𝐶 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
129 nfcv ⊢ Ⅎ 𝑗 ( 𝐵 + 𝐶 )
130 nfcv ⊢ Ⅎ 𝑘 +
131 79 130 89 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
132 128 129 131 cbvsum ⊢ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) = Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
133 132 mpteq2i ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
134 133 rneqi ⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
135 134 supeq1i ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < )
136 135 eqcomi ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < )
137 136 a1i ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
138 137 26 eqtr4d ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
139 ge0xaddcl ⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
140 17 20 139 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
141 28 140 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ( 0 [,] +∞ ) )
142 6 1 141 sge0clmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) )
143 138 142 eqeltrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
144 127 143 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
145 112 4 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ )
146 127 145 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ )
147 121 5 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ )
148 127 147 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ )
149 74 88 96 97 100 103 106 108 117 126 144 146 148 sge0xaddlem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
150 112 121 oveq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
151 135 oveq1i ⊢ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +e 𝑒 )
152 150 151 breq12i ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) ↔ ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
153 149 152 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
154 153 3exp ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) ) ) )
155 154 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) ) )
156 72 155 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
157 156 3exp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) ) ) )
158 157 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) ) )
159 68 158 mpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
160 61 159 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +e 𝑒 ) )
161 40 59 160 xrlexaddrp ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
162 26 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
163 43 48 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → ( 𝐵 + 𝐶 ) ∈ ( 0 [,) +∞ ) )
164 42 163 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) = Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) )
165 49 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ℂ )
166 50 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐶 ∈ ℂ )
167 42 165 166 fsumadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) )
168 164 167 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) = ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) )
169 42 49 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ )
170 42 50 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ ℝ )
171 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) ∈ ℝ )
172 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ∈ ℝ )
173 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
174 173 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
175 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
176 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
177 176 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
178 simpr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑦 )
179 177 178 sseldd ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
180 179 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
181 175 180 12 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℝ )
182 174 181 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ )
183 182 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* )
184 183 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* )
185 eqid ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 )
186 185 rnmptss ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
187 184 186 syl ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
189 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
190 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 )
191 sumeq1 ⊢ ( 𝑦 = 𝑥 → Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 )
192 191 rspceeqv ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
193 189 190 192 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
194 169 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ V )
195 185 193 194 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) )
196 supxrub ⊢ ( ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* ∧ Σ 𝑘 ∈ 𝑥 𝐵 ∈ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) )
197 188 195 196 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) )
198 nfv ⊢ Ⅎ 𝑧 𝜑
199 eqid ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 )
200 elinel2 ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
201 200 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
202 simpll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝜑 )
203 elpwinss ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 )
204 203 adantr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑧 ⊆ 𝐴 )
205 simpr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝑧 )
206 204 205 sseldd ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝐴 )
207 206 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝐴 )
208 202 207 13 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝐶 ∈ ℝ )
209 201 208 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 𝐶 ∈ ℝ )
210 209 rexrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 𝐶 ∈ ℝ* )
211 198 199 210 rnmptssd ⊢ ( 𝜑 → ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* )
212 211 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* )
213 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 )
214 sumeq1 ⊢ ( 𝑧 = 𝑥 → Σ 𝑘 ∈ 𝑧 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 )
215 214 rspceeqv ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑧 𝐶 )
216 189 213 215 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑧 𝐶 )
217 170 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ V )
218 199 216 217 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) )
219 supxrub ⊢ ( ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* ∧ Σ 𝑘 ∈ 𝑥 𝐶 ∈ ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ≤ sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) )
220 212 218 219 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ≤ sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) )
221 169 170 171 172 197 220 le2addd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
222 168 221 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
223 222 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
224 6 1 141 40 sge0lefimpt ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ) )
225 223 224 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
226 162 225 eqbrtrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
227 40 59 161 226 xrletrid ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
228 32 35 227 3eqtrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
229 26 30 228 3eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )