## Stream: new members

### Topic: Simple induction proof

#### André Beyer (Jan 16 2021 at 15:08):

I'm struggling to complete this simple inductive proof below:

example (n i : ℕ) : 2 * (∑ k in finset.range n, i) = n * (n + 1) :=
begin
induction n with d hd,
{ simp, },
{
simp,
sorry,
}
end


I'll end up at the following state:

2 * i + d * (d + 1) = (d + 1) * (d + 2)


I'm particularly confused about finset.sum_range_succ. I was expecting to get d + 1 instead of i. Thanks in advance!

#### Shing Tak Lam (Jan 16 2021 at 15:11):

Is the statement correct? What you have is $2\sum_{k=0}^{n-1} i = n(n+1)$, not $2\sum_{k=0}^{n} k = n(n+1)$ (which is ∑ k in finset.range n.succ, k)

#### André Beyer (Jan 16 2021 at 16:05):

Right - embarrassingly. Thanks!

I'm still stuck after correction:

2 * d + d * (d + 1) = (d + 1) * (d + 2)


What would easily work is:

2 * (d + 1) + d * (d + 1) = (d + 1) * (d + 2)


I still don't understand why it's d and not d+1.

#### Bryan Gin-ge Chen (Jan 16 2021 at 16:10):

The i in the sum should be a k (and then i can be removed completely):

import algebra.big_operators.basic
import tactic

open_locale big_operators
example (n : ℕ) : 2 * (∑ k in finset.range (n + 1), k) = n * (n + 1) :=
begin
induction n with d hd,
{ simp, },
ring, }
end


#### André Beyer (Jan 16 2021 at 16:33):

Thanks, that works.

I still have problems understanding it though. I wanted to proof

$2 \cdot \sum_{k=1}^n k = n (n + 1)$

I would translate the working version as follows though:

$2 \cdot \sum_{k=1}^{n+1} k = n (n + 1)$

In what range does finset.range operate? Is it usually from 0 to n-1 and thus we'd write n + 1?

#### Bryan Gin-ge Chen (Jan 16 2021 at 16:35):

finset.range n is the finite set of numbers $\{0,1,2,\dots,n-1\}$ (cf. docs#finset.range), so the sum in my code (2 * (∑ k in finset.range (n + 1), k)) translates to:

$2 \cdot \sum_{k=0}^n k = n (n + 1)$

#### André Beyer (Jan 16 2021 at 16:43):

Nice, thank you!

Last updated: May 14 2021 at 07:19 UTC