# Zulip Chat Archive

## 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, },
{
rw [← nat.add_one, finset.sum_range_succ, mul_add, hd],
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, },
{ rw [← nat.add_one, finset.sum_range_succ, mul_add, hd],
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