| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fsumge0.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 2 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → 𝐴 ∈ Fin) | 
| 3 |  | fsumge0.2 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 4 | 3 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ 𝐴) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 5 |  | fsumge0.3 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) | 
| 6 | 5 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ 𝐴) ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) | 
| 7 |  | snssi 4807 | . . . . . . . . . 10
⊢ (𝑚 ∈ 𝐴 → {𝑚} ⊆ 𝐴) | 
| 8 | 7 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → {𝑚} ⊆ 𝐴) | 
| 9 | 2, 4, 6, 8 | fsumless 15833 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → Σ𝑘 ∈ {𝑚}𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) | 
| 10 | 9 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → Σ𝑘 ∈ {𝑚}𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) | 
| 11 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴) | 
| 12 | 3, 5 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | 
| 13 | 12 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) → ∀𝑘 ∈ 𝐴 (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | 
| 15 |  | nfcsb1v 3922 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 | 
| 16 | 15 | nfel1 2921 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ | 
| 17 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑘0 | 
| 18 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑘
≤ | 
| 19 | 17, 18, 15 | nfbr 5189 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘0 ≤
⦋𝑚 / 𝑘⦌𝐵 | 
| 20 | 16, 19 | nfan 1898 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘(⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑚 / 𝑘⦌𝐵) | 
| 21 |  | csbeq1a 3912 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵) | 
| 22 | 21 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ)) | 
| 23 | 21 | breq2d 5154 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑚 / 𝑘⦌𝐵)) | 
| 24 | 22, 23 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ↔ (⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑚 / 𝑘⦌𝐵))) | 
| 25 | 20, 24 | rspc 3609 | . . . . . . . . . . 11
⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → (⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑚 / 𝑘⦌𝐵))) | 
| 26 | 14, 25 | mpan9 506 | . . . . . . . . . 10
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → (⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑚 / 𝑘⦌𝐵)) | 
| 27 | 26 | simpld 494 | . . . . . . . . 9
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℝ) | 
| 28 | 27 | recnd 11290 | . . . . . . . 8
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) | 
| 29 |  | sumsns 15787 | . . . . . . . 8
⊢ ((𝑚 ∈ 𝐴 ∧ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑚}𝐵 = ⦋𝑚 / 𝑘⦌𝐵) | 
| 30 | 11, 28, 29 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → Σ𝑘 ∈ {𝑚}𝐵 = ⦋𝑚 / 𝑘⦌𝐵) | 
| 31 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → Σ𝑘 ∈ 𝐴 𝐵 = 0) | 
| 32 | 10, 30, 31 | 3brtr3d 5173 | . . . . . 6
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ≤ 0) | 
| 33 | 26 | simprd 495 | . . . . . 6
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → 0 ≤ ⦋𝑚 / 𝑘⦌𝐵) | 
| 34 |  | 0re 11264 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 35 |  | letri3 11347 | . . . . . . 7
⊢
((⦋𝑚 /
𝑘⦌𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → (⦋𝑚 / 𝑘⦌𝐵 = 0 ↔ (⦋𝑚 / 𝑘⦌𝐵 ≤ 0 ∧ 0 ≤ ⦋𝑚 / 𝑘⦌𝐵))) | 
| 36 | 27, 34, 35 | sylancl 586 | . . . . . 6
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → (⦋𝑚 / 𝑘⦌𝐵 = 0 ↔ (⦋𝑚 / 𝑘⦌𝐵 ≤ 0 ∧ 0 ≤ ⦋𝑚 / 𝑘⦌𝐵))) | 
| 37 | 32, 33, 36 | mpbir2and 713 | . . . . 5
⊢ (((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 = 0) | 
| 38 | 37 | ralrimiva 3145 | . . . 4
⊢ ((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) → ∀𝑚 ∈ 𝐴 ⦋𝑚 / 𝑘⦌𝐵 = 0) | 
| 39 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑚 𝐵 = 0 | 
| 40 | 15 | nfeq1 2920 | . . . . 5
⊢
Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 = 0 | 
| 41 | 21 | eqeq1d 2738 | . . . . 5
⊢ (𝑘 = 𝑚 → (𝐵 = 0 ↔ ⦋𝑚 / 𝑘⦌𝐵 = 0)) | 
| 42 | 39, 40, 41 | cbvralw 3305 | . . . 4
⊢
(∀𝑘 ∈
𝐴 𝐵 = 0 ↔ ∀𝑚 ∈ 𝐴 ⦋𝑚 / 𝑘⦌𝐵 = 0) | 
| 43 | 38, 42 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ Σ𝑘 ∈ 𝐴 𝐵 = 0) → ∀𝑘 ∈ 𝐴 𝐵 = 0) | 
| 44 | 43 | ex 412 | . 2
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 → ∀𝑘 ∈ 𝐴 𝐵 = 0)) | 
| 45 |  | sumz 15759 | . . . . 5
⊢ ((𝐴 ⊆
(ℤ≥‘0) ∨ 𝐴 ∈ Fin) → Σ𝑘 ∈ 𝐴 0 = 0) | 
| 46 | 45 | olcs 876 | . . . 4
⊢ (𝐴 ∈ Fin → Σ𝑘 ∈ 𝐴 0 = 0) | 
| 47 |  | sumeq2 15731 | . . . . 5
⊢
(∀𝑘 ∈
𝐴 𝐵 = 0 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 0) | 
| 48 | 47 | eqeq1d 2738 | . . . 4
⊢
(∀𝑘 ∈
𝐴 𝐵 = 0 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 ↔ Σ𝑘 ∈ 𝐴 0 = 0)) | 
| 49 | 46, 48 | syl5ibrcom 247 | . . 3
⊢ (𝐴 ∈ Fin →
(∀𝑘 ∈ 𝐴 𝐵 = 0 → Σ𝑘 ∈ 𝐴 𝐵 = 0)) | 
| 50 | 1, 49 | syl 17 | . 2
⊢ (𝜑 → (∀𝑘 ∈ 𝐴 𝐵 = 0 → Σ𝑘 ∈ 𝐴 𝐵 = 0)) | 
| 51 | 44, 50 | impbid 212 | 1
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀𝑘 ∈ 𝐴 𝐵 = 0)) |