![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fsumge0 | Structured version Visualization version Unicode version |
Description: If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
Ref | Expression |
---|---|
fsumge0.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fsumge0.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fsumge0.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fsumge0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rge0ssre 11768 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-resscn 9621 |
. . . . 5
![]() ![]() ![]() ![]() | |
3 | 1, 2 | sstri 3452 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | ge0addcl 11772 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | adantl 472 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | fsumge0.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | fsumge0.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | fsumge0.3 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | elrege0 11766 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 8, 9, 10 | sylanbrc 675 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 0e0icopnf 11770 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 12 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 4, 6, 7, 11, 13 | fsumcllem 13846 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | elrege0 11766 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 15 | simprbi 470 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 14, 16 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-rep 4528 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609 ax-inf2 8171 ax-cnex 9620 ax-resscn 9621 ax-1cn 9622 ax-icn 9623 ax-addcl 9624 ax-addrcl 9625 ax-mulcl 9626 ax-mulrcl 9627 ax-mulcom 9628 ax-addass 9629 ax-mulass 9630 ax-distr 9631 ax-i2m1 9632 ax-1ne0 9633 ax-1rid 9634 ax-rnegex 9635 ax-rrecex 9636 ax-cnre 9637 ax-pre-lttri 9638 ax-pre-lttrn 9639 ax-pre-ltadd 9640 ax-pre-mulgt0 9641 ax-pre-sup 9642 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-fal 1460 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-nel 2635 df-ral 2753 df-rex 2754 df-reu 2755 df-rmo 2756 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-pss 3431 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-tp 3984 df-op 3986 df-uni 4212 df-int 4248 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-tr 4511 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-se 4812 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-isom 5609 df-riota 6276 df-ov 6317 df-oprab 6318 df-mpt2 6319 df-om 6719 df-1st 6819 df-2nd 6820 df-wrecs 7053 df-recs 7115 df-rdg 7153 df-1o 7207 df-oadd 7211 df-er 7388 df-en 7595 df-dom 7596 df-sdom 7597 df-fin 7598 df-sup 7981 df-oi 8050 df-card 8398 df-pnf 9702 df-mnf 9703 df-xr 9704 df-ltxr 9705 df-le 9706 df-sub 9887 df-neg 9888 df-div 10297 df-nn 10637 df-2 10695 df-3 10696 df-n0 10898 df-z 10966 df-uz 11188 df-rp 11331 df-ico 11669 df-fz 11813 df-fzo 11946 df-seq 12245 df-exp 12304 df-hash 12547 df-cj 13210 df-re 13211 df-im 13212 df-sqrt 13346 df-abs 13347 df-clim 13600 df-sum 13801 |
This theorem is referenced by: fsumless 13904 fsumle 13907 o1fsum 13921 rrxcph 22399 csbren 22401 trirn 22402 rrxmet 22410 rrxdstprj1 22411 itg1ge0 22692 itg1ge0a 22717 mtest 23407 abelthlem7 23441 abelthlem8 23442 ftalem4 24048 ftalem5 24049 ftalem4OLD 24050 ftalem5OLD 24051 chtge0 24087 vmadivsum 24368 vmadivsumb 24369 rpvmasumlem 24373 dchrvmasumlem2 24384 dchrisum0re 24399 rplogsum 24413 dirith2 24414 mulog2sumlem2 24421 vmalogdivsum2 24424 2vmadivsumlem 24426 selbergb 24435 selberg2b 24438 logdivbnd 24442 selberg3lem2 24444 selberg4lem1 24446 pntrlog2bndlem1 24463 pntrlog2bndlem2 24464 pntrlog2bnd 24470 pntpbnd1 24472 pntlemf 24491 axsegconlem3 24997 ax5seglem3 25009 sibfof 29221 eulerpartlemgc 29243 eulerpartlemb 29249 rrnmet 32205 rrndstprj1 32206 rrndstprj2 32207 fsumge0cl 37689 stoweidlem26 37923 stoweidlem38 37936 stoweidlem44 37942 etransclem35 38171 rrndistlt 38196 hoiqssbllem2 38482 |
Copyright terms: Public domain | W3C validator |