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 ) )