Metamath Proof Explorer

Theorem fsum00

Description: A sum of nonnegative numbers is zero iff all terms are zero. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumge0.1 
|- ( ph -> A e. Fin )
fsumge0.2 
|- ( ( ph /\ k e. A ) -> B e. RR )
fsumge0.3 
|- ( ( ph /\ k e. A ) -> 0 <_ B )
Assertion fsum00 
|- ( ph -> ( sum_ k e. A B = 0 <-> A. k e. A B = 0 ) )

Proof

Step Hyp Ref Expression
1 fsumge0.1 
 |-  ( ph -> A e. Fin )
2 fsumge0.2 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
3 fsumge0.3 
 |-  ( ( ph /\ k e. A ) -> 0 <_ B )
4 1 adantr 
 |-  ( ( ph /\ m e. A ) -> A e. Fin )
5 2 adantlr 
 |-  ( ( ( ph /\ m e. A ) /\ k e. A ) -> B e. RR )
6 3 adantlr 
 |-  ( ( ( ph /\ m e. A ) /\ k e. A ) -> 0 <_ B )
7 snssi 
 |-  ( m e. A -> { m } C_ A )
8 7 adantl 
 |-  ( ( ph /\ m e. A ) -> { m } C_ A )
9 4 5 6 8 fsumless 
 |-  ( ( ph /\ m e. A ) -> sum_ k e. { m } B <_ sum_ k e. A B )
10 9 adantlr 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. { m } B <_ sum_ k e. A B )
11 simpr 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> m e. A )
12 2 3 jca 
 |-  ( ( ph /\ k e. A ) -> ( B e. RR /\ 0 <_ B ) )
13 12 ralrimiva 
 |-  ( ph -> A. k e. A ( B e. RR /\ 0 <_ B ) )
14 13 adantr 
 |-  ( ( ph /\ sum_ k e. A B = 0 ) -> A. k e. A ( B e. RR /\ 0 <_ B ) )
15 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
16 15 nfel1 
 |-  F/ k [_ m / k ]_ B e. RR
17 nfcv 
 |-  F/_ k 0
18 nfcv 
 |-  F/_ k <_
19 17 18 15 nfbr 
 |-  F/ k 0 <_ [_ m / k ]_ B
20 16 19 nfan 
 |-  F/ k ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B )
21 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
22 21 eleq1d 
 |-  ( k = m -> ( B e. RR <-> [_ m / k ]_ B e. RR ) )
23 21 breq2d 
 |-  ( k = m -> ( 0 <_ B <-> 0 <_ [_ m / k ]_ B ) )
24 22 23 anbi12d 
 |-  ( k = m -> ( ( B e. RR /\ 0 <_ B ) <-> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) ) )
25 20 24 rspc 
 |-  ( m e. A -> ( A. k e. A ( B e. RR /\ 0 <_ B ) -> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) ) )
26 14 25 mpan9 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) )
27 26 simpld 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B e. RR )
28 27 recnd 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B e. CC )
29 sumsns 
 |-  ( ( m e. A /\ [_ m / k ]_ B e. CC ) -> sum_ k e. { m } B = [_ m / k ]_ B )
30 11 28 29 syl2anc 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. { m } B = [_ m / k ]_ B )
31 simplr 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. A B = 0 )
32 10 30 31 3brtr3d 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B <_ 0 )
33 26 simprd 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> 0 <_ [_ m / k ]_ B )
34 0re 
 |-  0 e. RR
35 letri3 
 |-  ( ( [_ m / k ]_ B e. RR /\ 0 e. RR ) -> ( [_ m / k ]_ B = 0 <-> ( [_ m / k ]_ B <_ 0 /\ 0 <_ [_ m / k ]_ B ) ) )
36 27 34 35 sylancl 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> ( [_ m / k ]_ B = 0 <-> ( [_ m / k ]_ B <_ 0 /\ 0 <_ [_ m / k ]_ B ) ) )
37 32 33 36 mpbir2and 
 |-  ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B = 0 )
38 37 ralrimiva 
 |-  ( ( ph /\ sum_ k e. A B = 0 ) -> A. m e. A [_ m / k ]_ B = 0 )
39 nfv 
 |-  F/ m B = 0
40 15 nfeq1 
 |-  F/ k [_ m / k ]_ B = 0
41 21 eqeq1d 
 |-  ( k = m -> ( B = 0 <-> [_ m / k ]_ B = 0 ) )
42 39 40 41 cbvralw 
 |-  ( A. k e. A B = 0 <-> A. m e. A [_ m / k ]_ B = 0 )
43 38 42 sylibr 
 |-  ( ( ph /\ sum_ k e. A B = 0 ) -> A. k e. A B = 0 )
44 43 ex 
 |-  ( ph -> ( sum_ k e. A B = 0 -> A. k e. A B = 0 ) )
45 sumz 
 |-  ( ( A C_ ( ZZ>= ` 0 ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )
46 45 olcs 
 |-  ( A e. Fin -> sum_ k e. A 0 = 0 )
47 sumeq2 
 |-  ( A. k e. A B = 0 -> sum_ k e. A B = sum_ k e. A 0 )
48 47 eqeq1d 
 |-  ( A. k e. A B = 0 -> ( sum_ k e. A B = 0 <-> sum_ k e. A 0 = 0 ) )
49 46 48 syl5ibrcom 
 |-  ( A e. Fin -> ( A. k e. A B = 0 -> sum_ k e. A B = 0 ) )
50 1 49 syl 
 |-  ( ph -> ( A. k e. A B = 0 -> sum_ k e. A B = 0 ) )
51 44 50 impbid 
 |-  ( ph -> ( sum_ k e. A B = 0 <-> A. k e. A B = 0 ) )