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 
|- ( ph -> A e. V )
sge0pr.b 
|- ( ph -> B e. W )
sge0pr.d 
|- ( ph -> D e. ( 0 [,] +oo ) )
sge0pr.e 
|- ( ph -> E e. ( 0 [,] +oo ) )
sge0pr.cd 
|- ( k = A -> C = D )
sge0pr.ce 
|- ( k = B -> C = E )
sge0pr.ab 
|- ( ph -> A =/= B )
Assertion sge0pr 
|- ( ph -> ( sum^ ` ( k e. { A , B } |-> C ) ) = ( D +e E ) )

Proof

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