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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
fsumge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion fsum00 ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀ 𝑘 ∈ 𝐴 𝐵 = 0 ) )

Proof

Step Hyp Ref Expression
1 fsumge0.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 fsumge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
4 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → 𝐴 ∈ Fin )
5 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
7 snssi ⊢ ( 𝑚 ∈ 𝐴 → { 𝑚 } ⊆ 𝐴 )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → { 𝑚 } ⊆ 𝐴 )
9 4 5 6 8 fsumless ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑚 } 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
10 9 adantlr ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑚 } 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
11 simpr ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ 𝐴 )
12 2 3 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) → ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
15 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵
16 15 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ
17 nfcv ⊢ Ⅎ 𝑘 0
18 nfcv ⊢ Ⅎ 𝑘 ≤
19 17 18 15 nfbr ⊢ Ⅎ 𝑘 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵
20 16 19 nfan ⊢ Ⅎ 𝑘 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
21 csbeq1a ⊢ ( 𝑘 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
22 21 eleq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
23 21 breq2d ⊢ ( 𝑘 = 𝑚 → ( 0 ≤ 𝐵 ↔ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
24 22 23 anbi12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ↔ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
25 20 24 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
26 14 25 mpan9 ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
27 26 simpld ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ )
28 27 recnd ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ )
29 sumsns ⊢ ( ( 𝑚 ∈ 𝐴 ∧ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑚 } 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
30 11 28 29 syl2anc ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑚 } 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
31 simplr ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐴 𝐵 = 0 )
32 10 30 31 3brtr3d ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ≤ 0 )
33 26 simprd ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
34 0re ⊢ 0 ∈ ℝ
35 letri3 ⊢ ( ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 ↔ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ≤ 0 ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
36 27 34 35 sylancl ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 ↔ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ≤ 0 ∧ 0 ≤ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
37 32 33 36 mpbir2and ⊢ ( ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 )
38 37 ralrimiva ⊢ ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) → ∀ 𝑚 ∈ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 )
39 nfv ⊢ Ⅎ 𝑚 𝐵 = 0
40 15 nfeq1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0
41 21 eqeq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐵 = 0 ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 ) )
42 39 40 41 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀ 𝑚 ∈ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = 0 )
43 38 42 sylibr ⊢ ( ( 𝜑 ∧ Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) → ∀ 𝑘 ∈ 𝐴 𝐵 = 0 )
44 43 ex ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 = 0 → ∀ 𝑘 ∈ 𝐴 𝐵 = 0 ) )
45 sumz ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝐴 ∈ Fin ) → Σ 𝑘 ∈ 𝐴 0 = 0 )
46 45 olcs ⊢ ( 𝐴 ∈ Fin → Σ 𝑘 ∈ 𝐴 0 = 0 )
47 sumeq2 ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 0 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 0 )
48 47 eqeq1d ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 0 → ( Σ 𝑘 ∈ 𝐴 𝐵 = 0 ↔ Σ 𝑘 ∈ 𝐴 0 = 0 ) )
49 46 48 syl5ibrcom ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑘 ∈ 𝐴 𝐵 = 0 → Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) )
50 1 49 syl ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ 𝐴 𝐵 = 0 → Σ 𝑘 ∈ 𝐴 𝐵 = 0 ) )
51 44 50 impbid ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀ 𝑘 ∈ 𝐴 𝐵 = 0 ) )