Metamath Proof Explorer

Theorem sge0prle

Description: The sum of a pair of nonnegative extended reals is less than or equal their extended addition. When it is a distinct pair, than equality holds, see sge0pr . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0prle.a 
|- ( ph -> A e. V )
sge0prle.b 
|- ( ph -> B e. W )
sge0prle.d 
|- ( ph -> D e. ( 0 [,] +oo ) )
sge0prle.e 
|- ( ph -> E e. ( 0 [,] +oo ) )
sge0prle.cd 
|- ( k = A -> C = D )
sge0prle.ce 
|- ( k = B -> C = E )
Assertion sge0prle 
|- ( ph -> ( sum^ ` ( k e. { A , B } |-> C ) ) <_ ( D +e E ) )

Proof

Step Hyp Ref Expression
1 sge0prle.a 
 |-  ( ph -> A e. V )
2 sge0prle.b 
 |-  ( ph -> B e. W )
3 sge0prle.d 
 |-  ( ph -> D e. ( 0 [,] +oo ) )
4 sge0prle.e 
 |-  ( ph -> E e. ( 0 [,] +oo ) )
5 sge0prle.cd 
 |-  ( k = A -> C = D )
6 sge0prle.ce 
 |-  ( k = B -> C = E )
7 preq1 
 |-  ( A = B -> { A , B } = { B , B } )
8 dfsn2 
 |-  { B } = { B , B }
9 8 eqcomi 
 |-  { B , B } = { B }
10 9 a1i 
 |-  ( A = B -> { B , B } = { B } )
11 7 10 eqtrd 
 |-  ( A = B -> { A , B } = { B } )
12 11 mpteq1d 
 |-  ( A = B -> ( k e. { A , B } |-> C ) = ( k e. { B } |-> C ) )
13 12 fveq2d 
 |-  ( A = B -> ( sum^ ` ( k e. { A , B } |-> C ) ) = ( sum^ ` ( k e. { B } |-> C ) ) )
14 13 adantl 
 |-  ( ( ph /\ A = B ) -> ( sum^ ` ( k e. { A , B } |-> C ) ) = ( sum^ ` ( k e. { B } |-> C ) ) )
15 2 4 6 sge0snmpt 
 |-  ( ph -> ( sum^ ` ( k e. { B } |-> C ) ) = E )
16 15 adantr 
 |-  ( ( ph /\ A = B ) -> ( sum^ ` ( k e. { B } |-> C ) ) = E )
17 14 16 eqtrd 
 |-  ( ( ph /\ A = B ) -> ( sum^ ` ( k e. { A , B } |-> C ) ) = E )
18 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
19 18 4 sselid 
 |-  ( ph -> E e. RR* )
20 19 xaddlidd 
 |-  ( ph -> ( 0 +e E ) = E )
21 20 eqcomd 
 |-  ( ph -> E = ( 0 +e E ) )
22 0xr 
 |-  0 e. RR*
23 22 a1i 
 |-  ( ph -> 0 e. RR* )
24 18 3 sselid 
 |-  ( ph -> D e. RR* )
25 pnfxr 
 |-  +oo e. RR*
26 25 a1i 
 |-  ( ph -> +oo e. RR* )
27 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ D e. ( 0 [,] +oo ) ) -> 0 <_ D )
28 23 26 3 27 syl3anc 
 |-  ( ph -> 0 <_ D )
29 23 24 19 28 xleadd1d 
 |-  ( ph -> ( 0 +e E ) <_ ( D +e E ) )
30 21 29 eqbrtrd 
 |-  ( ph -> E <_ ( D +e E ) )
31 30 adantr 
 |-  ( ( ph /\ A = B ) -> E <_ ( D +e E ) )
32 17 31 eqbrtrd 
 |-  ( ( ph /\ A = B ) -> ( sum^ ` ( k e. { A , B } |-> C ) ) <_ ( D +e E ) )
33 1 adantr 
 |-  ( ( ph /\ -. A = B ) -> A e. V )
34 2 adantr 
 |-  ( ( ph /\ -. A = B ) -> B e. W )
35 3 adantr 
 |-  ( ( ph /\ -. A = B ) -> D e. ( 0 [,] +oo ) )
36 4 adantr 
 |-  ( ( ph /\ -. A = B ) -> E e. ( 0 [,] +oo ) )
37 neqne 
 |-  ( -. A = B -> A =/= B )
38 37 adantl 
 |-  ( ( ph /\ -. A = B ) -> A =/= B )
39 33 34 35 36 5 6 38 sge0pr 
 |-  ( ( ph /\ -. A = B ) -> ( sum^ ` ( k e. { A , B } |-> C ) ) = ( D +e E ) )
40 24 19 xaddcld 
 |-  ( ph -> ( D +e E ) e. RR* )
41 40 xrleidd 
 |-  ( ph -> ( D +e E ) <_ ( D +e E ) )
42 41 adantr 
 |-  ( ( ph /\ -. A = B ) -> ( D +e E ) <_ ( D +e E ) )
43 39 42 eqbrtrd 
 |-  ( ( ph /\ -. A = B ) -> ( sum^ ` ( k e. { A , B } |-> C ) ) <_ ( D +e E ) )
44 32 43 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( k e. { A , B } |-> C ) ) <_ ( D +e E ) )