Metamath Proof Explorer

Theorem sge0pr

Description: Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0pr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0pr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
sge0pr.d ⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
sge0pr.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
sge0pr.cd ⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
sge0pr.ce ⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
sge0pr.ab ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion sge0pr ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )

Proof

Step Hyp Ref Expression
1 sge0pr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0pr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 sge0pr.d ⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
4 sge0pr.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
5 sge0pr.cd ⊢ ( 𝑘 = 𝐴 → 𝐶 = 𝐷 )
6 sge0pr.ce ⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐸 )
7 sge0pr.ab ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
8 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
9 8 4 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
10 mnfxr ⊢ -∞ ∈ ℝ*
11 10 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
12 0xr ⊢ 0 ∈ ℝ*
13 12 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
14 mnflt0 ⊢ -∞ < 0
15 14 a1i ⊢ ( 𝜑 → -∞ < 0 )
16 pnfxr ⊢ +∞ ∈ ℝ*
17 16 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
18 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐸 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐸 )
19 13 17 4 18 syl3anc ⊢ ( 𝜑 → 0 ≤ 𝐸 )
20 11 13 9 15 19 xrltletrd ⊢ ( 𝜑 → -∞ < 𝐸 )
21 11 9 20 xrgtned ⊢ ( 𝜑 → 𝐸 ≠ -∞ )
22 xaddpnf2 ⊢ ( ( 𝐸 ∈ ℝ* ∧ 𝐸 ≠ -∞ ) → ( +∞ +𝑒 𝐸 ) = +∞ )
23 9 21 22 syl2anc ⊢ ( 𝜑 → ( +∞ +𝑒 𝐸 ) = +∞ )
24 23 eqcomd ⊢ ( 𝜑 → +∞ = ( +∞ +𝑒 𝐸 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → +∞ = ( +∞ +𝑒 𝐸 ) )
26 prex ⊢ { 𝐴 , 𝐵 } ∈ V
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → { 𝐴 , 𝐵 } ∈ V )
28 5 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
29 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
30 28 29 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
32 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝜑 )
33 simpl ⊢ ( ( 𝑘 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑘 = 𝐴 ) → 𝑘 ∈ { 𝐴 , 𝐵 } )
34 neqne ⊢ ( ¬ 𝑘 = 𝐴 → 𝑘 ≠ 𝐴 )
35 34 adantl ⊢ ( ( 𝑘 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑘 = 𝐴 ) → 𝑘 ≠ 𝐴 )
36 elprn1 ⊢ ( ( 𝑘 ∈ { 𝐴 , 𝐵 } ∧ 𝑘 ≠ 𝐴 ) → 𝑘 = 𝐵 )
37 33 35 36 syl2anc ⊢ ( ( 𝑘 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑘 = 𝐴 ) → 𝑘 = 𝐵 )
38 37 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝑘 = 𝐵 )
39 6 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐸 ∈ ( 0 [,] +∞ ) )
41 39 40 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
42 32 38 41 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
43 31 42 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
44 eqid ⊢ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) = ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 )
45 43 44 fmptd ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) : { 𝐴 , 𝐵 } ⟶ ( 0 [,] +∞ ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) : { 𝐴 , 𝐵 } ⟶ ( 0 [,] +∞ ) )
47 id ⊢ ( 𝐷 = +∞ → 𝐷 = +∞ )
48 47 eqcomd ⊢ ( 𝐷 = +∞ → +∞ = 𝐷 )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → +∞ = 𝐷 )
50 prid1g ⊢ ( 𝐷 ∈ ( 0 [,] +∞ ) → 𝐷 ∈ { 𝐷 , 𝐸 } )
51 3 50 syl ⊢ ( 𝜑 → 𝐷 ∈ { 𝐷 , 𝐸 } )
52 1 2 44 5 6 rnmptpr ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) = { 𝐷 , 𝐸 } )
53 52 eqcomd ⊢ ( 𝜑 → { 𝐷 , 𝐸 } = ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
54 51 53 eleqtrd ⊢ ( 𝜑 → 𝐷 ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → 𝐷 ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
56 49 55 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → +∞ ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
57 27 46 56 sge0pnfval ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = +∞ )
58 oveq1 ⊢ ( 𝐷 = +∞ → ( 𝐷 +𝑒 𝐸 ) = ( +∞ +𝑒 𝐸 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → ( 𝐷 +𝑒 𝐸 ) = ( +∞ +𝑒 𝐸 ) )
60 25 57 59 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐷 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
61 8 3 sselid ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
62 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐷 )
63 13 17 3 62 syl3anc ⊢ ( 𝜑 → 0 ≤ 𝐷 )
64 11 13 61 15 63 xrltletrd ⊢ ( 𝜑 → -∞ < 𝐷 )
65 11 61 64 xrgtned ⊢ ( 𝜑 → 𝐷 ≠ -∞ )
66 xaddpnf1 ⊢ ( ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) → ( 𝐷 +𝑒 +∞ ) = +∞ )
67 61 65 66 syl2anc ⊢ ( 𝜑 → ( 𝐷 +𝑒 +∞ ) = +∞ )
68 67 eqcomd ⊢ ( 𝜑 → +∞ = ( 𝐷 +𝑒 +∞ ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → +∞ = ( 𝐷 +𝑒 +∞ ) )
70 26 a1i ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → { 𝐴 , 𝐵 } ∈ V )
71 45 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) : { 𝐴 , 𝐵 } ⟶ ( 0 [,] +∞ ) )
72 id ⊢ ( 𝐸 = +∞ → 𝐸 = +∞ )
73 72 eqcomd ⊢ ( 𝐸 = +∞ → +∞ = 𝐸 )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → +∞ = 𝐸 )
75 prid2g ⊢ ( 𝐸 ∈ ( 0 [,] +∞ ) → 𝐸 ∈ { 𝐷 , 𝐸 } )
76 4 75 syl ⊢ ( 𝜑 → 𝐸 ∈ { 𝐷 , 𝐸 } )
77 76 53 eleqtrd ⊢ ( 𝜑 → 𝐸 ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → 𝐸 ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
79 74 78 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → +∞ ∈ ran ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) )
80 70 71 79 sge0pnfval ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = +∞ )
81 oveq2 ⊢ ( 𝐸 = +∞ → ( 𝐷 +𝑒 𝐸 ) = ( 𝐷 +𝑒 +∞ ) )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → ( 𝐷 +𝑒 𝐸 ) = ( 𝐷 +𝑒 +∞ ) )
83 69 80 82 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
84 83 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ 𝐸 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
85 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
86 ax-resscn ⊢ ℝ ⊆ ℂ
87 85 86 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
88 12 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 0 ∈ ℝ* )
89 16 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → +∞ ∈ ℝ* )
90 61 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 𝐷 ∈ ℝ* )
91 63 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 0 ≤ 𝐷 )
92 pnfge ⊢ ( 𝐷 ∈ ℝ* → 𝐷 ≤ +∞ )
93 61 92 syl ⊢ ( 𝜑 → 𝐷 ≤ +∞ )
94 93 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 𝐷 ≤ +∞ )
95 47 necon3bi ⊢ ( ¬ 𝐷 = +∞ → 𝐷 ≠ +∞ )
96 95 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 𝐷 ≠ +∞ )
97 90 89 94 96 xrleneltd ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 𝐷 < +∞ )
98 88 89 90 91 97 elicod ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → 𝐷 ∈ ( 0 [,) +∞ ) )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐷 ∈ ( 0 [,) +∞ ) )
100 87 99 sselid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐷 ∈ ℂ )
101 12 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 0 ∈ ℝ* )
102 16 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → +∞ ∈ ℝ* )
103 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ℝ* )
104 19 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 0 ≤ 𝐸 )
105 pnfge ⊢ ( 𝐸 ∈ ℝ* → 𝐸 ≤ +∞ )
106 9 105 syl ⊢ ( 𝜑 → 𝐸 ≤ +∞ )
107 106 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ≤ +∞ )
108 72 necon3bi ⊢ ( ¬ 𝐸 = +∞ → 𝐸 ≠ +∞ )
109 108 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ≠ +∞ )
110 103 102 107 109 xrleneltd ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 < +∞ )
111 101 102 103 104 110 elicod ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ( 0 [,) +∞ ) )
112 87 111 sselid ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ℂ )
113 112 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ℂ )
114 100 113 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) )
115 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
116 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
117 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐴 ≠ 𝐵 )
118 5 6 114 116 117 sumpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 + 𝐸 ) )
119 prfi ⊢ { 𝐴 , 𝐵 } ∈ Fin
120 119 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → { 𝐴 , 𝐵 } ∈ Fin )
121 5 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
122 98 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ( 0 [,) +∞ ) )
123 121 122 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
124 123 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
125 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝜑 )
126 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → ¬ 𝐸 = +∞ )
127 37 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝑘 = 𝐵 )
128 39 3adant2 ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
129 111 3adant3 ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ∧ 𝑘 = 𝐵 ) → 𝐸 ∈ ( 0 [,) +∞ ) )
130 128 129 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ∧ 𝑘 = 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
131 125 126 127 130 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) ∧ ¬ 𝑘 = 𝐴 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
132 124 131 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝐶 ∈ ( 0 [,) +∞ ) )
133 120 132 sge0fsummpt ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 )
134 85 99 sselid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐷 ∈ ℝ )
135 85 111 sselid ⊢ ( ( 𝜑 ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ℝ )
136 135 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → 𝐸 ∈ ℝ )
137 rexadd ⊢ ( ( 𝐷 ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( 𝐷 +𝑒 𝐸 ) = ( 𝐷 + 𝐸 ) )
138 134 136 137 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → ( 𝐷 +𝑒 𝐸 ) = ( 𝐷 + 𝐸 ) )
139 118 133 138 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) ∧ ¬ 𝐸 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
140 84 139 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝐷 = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )
141 60 140 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ 𝐶 ) ) = ( 𝐷 +𝑒 𝐸 ) )