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