Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  serge0 Structured version   Unicode version

Theorem serge0 11377
 Description: A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)
Hypotheses
Ref Expression
serge0.1
serge0.2
serge0.3
Assertion
Ref Expression
serge0
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem serge0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 serge0.1 . . 3
2 serge0.2 . . . 4
3 serge0.3 . . . 4
4 breq2 4216 . . . . 5
54elrab 3092 . . . 4
62, 3, 5sylanbrc 646 . . 3
7 breq2 4216 . . . . . 6
87elrab 3092 . . . . 5
9 breq2 4216 . . . . . 6
109elrab 3092 . . . . 5
11 readdcl 9073 . . . . . . 7
1211ad2ant2r 728 . . . . . 6
13 addge0 9517 . . . . . . 7
1413an4s 800 . . . . . 6
15 breq2 4216 . . . . . . 7
1615elrab 3092 . . . . . 6
1712, 14, 16sylanbrc 646 . . . . 5
188, 10, 17syl2anb 466 . . . 4