Metamath Proof Explorer


Theorem sge0xadd

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

Ref Expression
Hypotheses sge0xadd.kph 𝑘 𝜑
sge0xadd.a ( 𝜑𝐴𝑉 )
sge0xadd.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
sge0xadd.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion sge0xadd ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0xadd.kph 𝑘 𝜑
2 sge0xadd.a ( 𝜑𝐴𝑉 )
3 sge0xadd.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4 sge0xadd.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 simpr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ )
6 5 oveq1d ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = ( +∞ +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
7 1 2 4 sge0xrclmpt ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ* )
8 eqid ( 𝑘𝐴𝐶 ) = ( 𝑘𝐴𝐶 )
9 1 4 8 fmptdf ( 𝜑 → ( 𝑘𝐴𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
10 2 9 sge0nemnf ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ≠ -∞ )
11 xaddpnf2 ( ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ≠ -∞ ) → ( +∞ +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = +∞ )
12 7 10 11 syl2anc ( 𝜑 → ( +∞ +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = +∞ )
13 12 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( +∞ +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = +∞ )
14 ge0xaddcl ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
15 3 4 14 syl2anc ( ( 𝜑𝑘𝐴 ) → ( 𝐵 +𝑒 𝐶 ) ∈ ( 0 [,] +∞ ) )
16 1 2 15 sge0xrclmpt ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) ∈ ℝ* )
17 16 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) ∈ ℝ* )
18 id ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ )
19 18 eqcomd ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) )
20 19 adantl ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) )
21 2 elexd ( 𝜑𝐴 ∈ V )
22 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
23 22 3 sseldi ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℝ* )
24 23 4 xadd0ge ( ( 𝜑𝑘𝐴 ) → 𝐵 ≤ ( 𝐵 +𝑒 𝐶 ) )
25 1 21 3 15 24 sge0lempt ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
26 25 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
27 20 26 eqbrtrd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → +∞ ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
28 17 27 xrgepnfd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = +∞ )
29 28 eqcomd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
30 6 13 29 3eqtrrd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
31 simpl ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → 𝜑 )
32 simpr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ )
33 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
34 1 3 33 fmptdf ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
35 2 34 sge0repnf ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) )
36 35 adantr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) )
37 32 36 mpbird ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ )
38 simpr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ )
39 38 oveq2d ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 +∞ ) )
40 2 34 sge0xrcl ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ* )
41 2 34 sge0nemnf ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ≠ -∞ )
42 xaddpnf1 ( ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ≠ -∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 +∞ ) = +∞ )
43 40 41 42 syl2anc ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 +∞ ) = +∞ )
44 43 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 +∞ ) = +∞ )
45 16 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) ∈ ℝ* )
46 id ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ )
47 46 eqcomd ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) )
48 47 adantl ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) )
49 22 4 sseldi ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℝ* )
50 49 3 xadd0ge2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ≤ ( 𝐵 +𝑒 𝐶 ) )
51 1 2 4 15 50 sge0lempt ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
52 51 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
53 48 52 eqbrtrd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → +∞ ≤ ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
54 45 53 xrgepnfd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = +∞ )
55 54 eqcomd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) )
56 39 44 55 3eqtrrd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
57 56 adantlr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
58 simpl ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) )
59 simpr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ )
60 2 9 sge0repnf ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) )
61 60 adantr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) )
62 59 61 mpbird ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ )
63 62 adantlr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ )
64 2 ad2antrr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → 𝐴𝑉 )
65 nfcv 𝑘 Σ^
66 nfmpt1 𝑘 ( 𝑘𝐴𝐵 )
67 65 66 nffv 𝑘 ( Σ^ ‘ ( 𝑘𝐴𝐵 ) )
68 nfcv 𝑘
69 67 68 nfel 𝑘 ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ
70 1 69 nfan 𝑘 ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ )
71 nfv 𝑘 𝑗𝐴
72 70 71 nfan 𝑘 ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑗𝐴 )
73 nfcsb1v 𝑘 𝑗 / 𝑘 𝐵
74 73 nfel1 𝑘 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ )
75 72 74 nfim 𝑘 ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ ) )
76 eleq1w ( 𝑘 = 𝑗 → ( 𝑘𝐴𝑗𝐴 ) )
77 76 anbi2d ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) ↔ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) ) )
78 csbeq1a ( 𝑘 = 𝑗𝐵 = 𝑗 / 𝑘 𝐵 )
79 78 eleq1d ( 𝑘 = 𝑗 → ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ ) ) )
80 77 79 imbi12d ( 𝑘 = 𝑗 → ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) ↔ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ ) ) ) )
81 2 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) → 𝐴𝑉 )
82 3 adantlr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
83 simpr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ )
84 70 81 82 83 sge0rernmpt ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
85 75 80 84 chvarfv ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ ) )
86 85 adantlr ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐵 ∈ ( 0 [,) +∞ ) )
87 nfmpt1 𝑘 ( 𝑘𝐴𝐶 )
88 65 87 nffv 𝑘 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) )
89 88 68 nfel 𝑘 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ
90 1 89 nfan 𝑘 ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ )
91 90 71 nfan 𝑘 ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 )
92 nfcsb1v 𝑘 𝑗 / 𝑘 𝐶
93 92 nfel1 𝑘 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ )
94 91 93 nfim 𝑘 ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ ) )
95 76 anbi2d ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) ↔ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) ) )
96 csbeq1a ( 𝑘 = 𝑗𝐶 = 𝑗 / 𝑘 𝐶 )
97 96 eleq1d ( 𝑘 = 𝑗 → ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ ) ) )
98 95 97 imbi12d ( 𝑘 = 𝑗 → ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) ) ↔ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ ) ) ) )
99 2 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → 𝐴𝑉 )
100 4 adantlr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
101 simpr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ )
102 90 99 100 101 sge0rernmpt ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
103 94 98 102 chvarfv ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ ) )
104 103 adantllr ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) ∧ 𝑗𝐴 ) → 𝑗 / 𝑘 𝐶 ∈ ( 0 [,) +∞ ) )
105 nfcv 𝑗 𝐵
106 105 73 78 cbvmpt ( 𝑘𝐴𝐵 ) = ( 𝑗𝐴 𝑗 / 𝑘 𝐵 )
107 106 fveq2i ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐵 ) )
108 simplr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ )
109 107 108 eqeltrrid ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐵 ) ) ∈ ℝ )
110 nfcv 𝑗 𝐶
111 110 92 96 cbvmpt ( 𝑘𝐴𝐶 ) = ( 𝑗𝐴 𝑗 / 𝑘 𝐶 )
112 111 fveq2i ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐶 ) )
113 simpr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ )
114 112 113 eqeltrrid ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐶 ) ) ∈ ℝ )
115 64 86 104 109 114 sge0xaddlem2 ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗𝐴 ↦ ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐶 ) ) ) )
116 nfcv 𝑗 ( 𝐵 +𝑒 𝐶 )
117 nfcv 𝑘 +𝑒
118 73 117 92 nfov 𝑘 ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 )
119 78 96 oveq12d ( 𝑘 = 𝑗 → ( 𝐵 +𝑒 𝐶 ) = ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 ) )
120 116 118 119 cbvmpt ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) = ( 𝑗𝐴 ↦ ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 ) )
121 120 fveq2i ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑗𝐴 ↦ ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 ) ) )
122 107 112 oveq12i ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐶 ) ) )
123 121 122 eqeq12i ( ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) ↔ ( Σ^ ‘ ( 𝑗𝐴 ↦ ( 𝑗 / 𝑘 𝐵 +𝑒 𝑗 / 𝑘 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑗𝐴 𝑗 / 𝑘 𝐶 ) ) ) )
124 115 123 sylibr ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
125 58 63 124 syl2anc ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
126 57 125 pm2.61dan ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
127 31 37 126 syl2anc ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )
128 30 127 pm2.61dan ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴 ↦ ( 𝐵 +𝑒 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) +𝑒 ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ) )