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

Proof

Step Hyp Ref Expression
1 sge0xadd.kph ⊢ Ⅎ 𝑘 𝜑
2 sge0xadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 sge0xadd.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4 sge0xadd.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 simpr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
6 5 oveq1d ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( +∞ +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
7 1 2 4 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* )
8 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
9 1 4 8 fmptdf ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
10 2 9 sge0nemnf ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ≠ -∞ )
11 xaddpnf2 ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ≠ -∞ ) → ( +∞ +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = +∞ )
12 7 10 11 syl2anc ⊢ ( 𝜑 → ( +∞ +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = +∞ )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( +∞ +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = +∞ )
14 ge0xaddcl ⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
15 3 4 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 +e 𝐶 ) ∈ ( 0 [,] +∞ ) )
16 1 2 15 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) ∈ ℝ* )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) ∈ ℝ* )
18 id ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
19 18 eqcomd ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
21 2 elexd ⊢ ( 𝜑 → 𝐴 ∈ V )
22 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
23 22 3 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
24 23 4 xadd0ge ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ ( 𝐵 +e 𝐶 ) )
25 1 21 3 15 24 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
27 20 26 eqbrtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → +∞ ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
28 17 27 xrgepnfd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = +∞ )
29 28 eqcomd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
30 6 13 29 3eqtrrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
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 ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e +∞ ) )
40 2 34 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )
41 2 34 sge0nemnf ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ≠ -∞ )
42 xaddpnf1 ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ≠ -∞ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e +∞ ) = +∞ )
43 40 41 42 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e +∞ ) = +∞ )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e +∞ ) = +∞ )
45 16 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) ∈ ℝ* )
46 id ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ )
47 46 eqcomd ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
49 22 4 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
50 49 3 xadd0ge2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ≤ ( 𝐵 +e 𝐶 ) )
51 1 2 4 15 50 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
53 48 52 eqbrtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → +∞ ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
54 45 53 xrgepnfd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = +∞ )
55 54 eqcomd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) )
56 39 44 55 3eqtrrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
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 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) )
116 nfcv ⊢ Ⅎ 𝑗 ( 𝐵 +e 𝐶 )
117 nfcv ⊢ Ⅎ 𝑘 +e
118 73 117 92 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
119 78 96 oveq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 +e 𝐶 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
120 116 118 119 cbvmpt ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) = ( 𝑗 ∈ 𝐴 ↦ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
121 120 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
122 107 112 oveq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
123 121 122 eqeq12i ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) ↔ ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 +e ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) )
124 115 123 sylibr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
125 58 63 124 syl2anc ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
126 57 125 pm2.61dan ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
127 31 37 126 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )
128 30 127 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 +e 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) +e ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) ) )