Description: The finite sum of A ( k ) from k = M to M (i.e. a sum with only one term) is B i.e. A ( M ) . (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 21-Apr-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | fsum1.1 | ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 ) | |
| Assertion | fsum1 | ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsum1.1 | ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 ) | |
| 2 | fzsn | ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } ) | |
| 3 | 2 | adantr | ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } ) |
| 4 | 3 | sumeq1d | ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = Σ 𝑘 ∈ { 𝑀 } 𝐴 ) |
| 5 | 1 | sumsn | ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 ) |
| 6 | 4 5 | eqtrd | ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = 𝐵 ) |