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 xaddid2d
 |-  ( 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 ) )