Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0prle Structured version   Visualization version   Unicode version

Theorem sge0prle 38357
 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 38350. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0prle.a
sge0prle.b
sge0prle.d
sge0prle.e
sge0prle.cd
sge0prle.ce
Assertion
Ref Expression
sge0prle Σ^
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem sge0prle
StepHypRef Expression
1 preq1 4042 . . . . . . . 8
2 dfsn2 3972 . . . . . . . . . 10
32eqcomi 2480 . . . . . . . . 9
43a1i 11 . . . . . . . 8
51, 4eqtrd 2505 . . . . . . 7
65mpteq1d 4477 . . . . . 6
76fveq2d 5883 . . . . 5 Σ^ Σ^
87adantl 473 . . . 4 Σ^ Σ^
9 sge0prle.b . . . . . 6
10 sge0prle.e . . . . . 6
11 sge0prle.ce . . . . . 6
129, 10, 11sge0snmpt 38339 . . . . 5 Σ^
1312adantr 472 . . . 4 Σ^
148, 13eqtrd 2505 . . 3 Σ^
15 iccssxr 11742 . . . . . . . 8
1615, 10sseldi 3416 . . . . . . 7
1716xaddid2d 37629 . . . . . 6
1817eqcomd 2477 . . . . 5
19 0xr 9705 . . . . . . 7
2019a1i 11 . . . . . 6
21 sge0prle.d . . . . . . 7
2215, 21sseldi 3416 . . . . . 6
23 pnfxr 11435 . . . . . . . 8
2423a1i 11 . . . . . . 7
25 iccgelb 11716 . . . . . . 7
2620, 24, 21, 25syl3anc 1292 . . . . . 6
2720, 22, 16, 26xleadd1d 37639 . . . . 5
2818, 27eqbrtrd 4416 . . . 4
3014, 29eqbrtrd 4416 . 2 Σ^
31 sge0prle.a . . . . 5
3231adantr 472 . . . 4
339adantr 472 . . . 4
3421adantr 472 . . . 4
3510adantr 472 . . . 4
36 sge0prle.cd . . . 4
37 neqne 2651 . . . . 5
3837adantl 473 . . . 4
3932, 33, 34, 35, 36, 11, 38sge0pr 38350 . . 3 Σ^
4022, 16xaddcld 11612 . . . . 5
41 xrleid 11472 . . . . 5
4240, 41syl 17 . . . 4