Metamath Proof Explorer


Theorem isumge0

Description: An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypotheses isumrecl.1 Z=M
isumrecl.2 φM
isumrecl.3 φkZFk=A
isumrecl.4 φkZA
isumrecl.5 φseqM+Fdom
isumge0.6 φkZ0A
Assertion isumge0 φ0kZA

Proof

Step Hyp Ref Expression
1 isumrecl.1 Z=M
2 isumrecl.2 φM
3 isumrecl.3 φkZFk=A
4 isumrecl.4 φkZA
5 isumrecl.5 φseqM+Fdom
6 isumge0.6 φkZ0A
7 4 recnd φkZA
8 1 2 3 7 5 isumclim2 φseqM+FkZA
9 fveq2 j=kFj=Fk
10 9 cbvsumv jZFj=kZFk
11 3 sumeq2dv φkZFk=kZA
12 10 11 eqtrid φjZFj=kZA
13 8 12 breqtrrd φseqM+FjZFj
14 3 4 eqeltrd φkZFk
15 6 3 breqtrrd φkZ0Fk
16 1 2 13 14 15 iserge0 φ0jZFj
17 16 12 breqtrd φ0kZA