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 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )

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 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
13 11 3 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
14 12 13 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
15 14 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ* )
16 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
17 16 2 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
18 xrge0ge0 ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝐵 )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
20 16 3 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 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 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 + 𝐶 ) )
28 12 13 27 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 + 𝐶 ) )
29 28 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
31 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
32 4 5 31 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
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 nfcv ⊢ Ⅎ 𝑗 𝑢
114 nfcv ⊢ Ⅎ 𝑘 𝑢
115 84 113 114 110 79 cbvsum ⊢ Σ 𝑘 ∈ 𝑢 𝐵 = Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
116 115 oveq1i ⊢ ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) = ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) )
117 112 116 breq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
118 117 biimpi ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
119 109 118 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) < ( Σ 𝑗 ∈ 𝑢 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ( 𝑒 / 2 ) ) )
120 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) )
121 nfcv ⊢ Ⅎ 𝑗 𝐶
122 121 89 92 cbvmpt ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
123 122 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
124 nfcv ⊢ Ⅎ 𝑗 𝑣
125 nfcv ⊢ Ⅎ 𝑘 𝑣
126 92 124 125 121 89 cbvsum ⊢ Σ 𝑘 ∈ 𝑣 𝐶 = Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
127 126 oveq1i ⊢ ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) = ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) )
128 123 127 breq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
129 128 biimpi ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
130 120 129 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) < ( Σ 𝑗 ∈ 𝑣 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 + ( 𝑒 / 2 ) ) )
131 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → 𝜑 )
132 84 92 oveq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 + 𝐶 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
133 nfcv ⊢ Ⅎ 𝑗 𝑥
134 nfcv ⊢ Ⅎ 𝑘 𝑥
135 nfcv ⊢ Ⅎ 𝑗 ( 𝐵 + 𝐶 )
136 nfcv ⊢ Ⅎ 𝑘 +
137 79 136 89 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
138 132 133 134 135 137 cbvsum ⊢ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) = Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
139 138 mpteq2i ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
140 139 rneqi ⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
141 140 supeq1i ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < )
142 141 eqcomi ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < )
143 142 a1i ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
144 143 26 eqtr4d ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
145 ge0xaddcl ⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
146 17 20 145 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
147 28 146 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ( 0 [,] +∞ ) )
148 6 1 147 sge0clmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) )
149 144 148 eqeltrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
150 131 149 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
151 112 4 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ )
152 131 151 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) ∈ ℝ )
153 123 5 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ )
154 131 153 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ )
155 74 88 96 97 100 103 106 108 119 130 150 152 154 sge0xaddlem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
156 112 123 oveq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
157 141 oveq1i ⊢ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 )
158 156 157 breq12i ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) ↔ ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) + ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑗 ∈ 𝑥 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 + ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
159 155 158 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) ∧ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
160 159 3exp ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) ) ) )
161 160 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) < ( Σ 𝑘 ∈ 𝑣 𝐶 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) ) )
162 72 161 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
163 162 3exp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) ) ) )
164 163 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑢 𝐵 + ( 𝑒 / 2 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) ) )
165 68 164 mpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) + ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
166 61 165 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ≤ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) +𝑒 𝑒 ) )
167 40 59 166 xrlexaddrp ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
168 26 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) )
169 43 48 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → ( 𝐵 + 𝐶 ) ∈ ( 0 [,) +∞ ) )
170 42 169 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) = Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) )
171 49 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ℂ )
172 50 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐶 ∈ ℂ )
173 42 171 172 fsumadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) )
174 170 173 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) = ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) )
175 42 49 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ )
176 42 50 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ ℝ )
177 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) ∈ ℝ )
178 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ∈ ℝ )
179 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
180 179 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
181 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
182 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
183 182 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
184 simpr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑦 )
185 183 184 sseldd ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
186 185 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
187 181 186 12 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℝ )
188 180 187 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ )
189 188 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* )
190 189 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* )
191 eqid ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 )
192 191 rnmptss ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ* → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
193 190 192 syl ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* )
195 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
196 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 )
197 sumeq1 ⊢ ( 𝑦 = 𝑥 → Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 )
198 197 rspceeqv ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
199 195 196 198 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ 𝑦 𝐵 )
200 175 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ V )
201 191 199 200 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) )
202 supxrub ⊢ ( ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ℝ* ∧ Σ 𝑘 ∈ 𝑥 𝐵 ∈ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) )
203 194 201 202 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) )
204 nfv ⊢ Ⅎ 𝑧 𝜑
205 eqid ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 )
206 elinel2 ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
207 206 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
208 simpll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝜑 )
209 elpwinss ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 )
210 209 adantr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑧 ⊆ 𝐴 )
211 simpr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝑧 )
212 210 211 sseldd ⊢ ( ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝐴 )
213 212 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝐴 )
214 208 213 13 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝐶 ∈ ℝ )
215 207 214 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 𝐶 ∈ ℝ )
216 215 rexrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 𝐶 ∈ ℝ* )
217 204 205 216 rnmptssd ⊢ ( 𝜑 → ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* )
218 217 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* )
219 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 )
220 sumeq1 ⊢ ( 𝑧 = 𝑥 → Σ 𝑘 ∈ 𝑧 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 )
221 220 rspceeqv ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑥 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑧 𝐶 )
222 195 219 221 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑘 ∈ 𝑥 𝐶 = Σ 𝑘 ∈ 𝑧 𝐶 )
223 176 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ V )
224 205 222 223 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ∈ ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) )
225 supxrub ⊢ ( ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ⊆ ℝ* ∧ Σ 𝑘 ∈ 𝑥 𝐶 ∈ ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ≤ sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) )
226 218 224 225 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐶 ≤ sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) )
227 175 176 177 178 203 226 le2addd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ 𝑘 ∈ 𝑥 𝐵 + Σ 𝑘 ∈ 𝑥 𝐶 ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
228 174 227 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
229 228 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
230 6 1 147 40 sge0lefimpt ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) ) )
231 229 230 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
232 168 231 eqbrtrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) )
233 40 59 167 232 xrletrid ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) + sup ( ran ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑧 𝐶 ) , ℝ* , < ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
234 32 35 233 3eqtrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 ( 𝐵 + 𝐶 ) ) , ℝ* , < ) )
235 26 30 234 3eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )