# Zulip Chat Archive

## Stream: new members

### Topic: silly computation with even numbers

#### Connor Gordon (Nov 01 2022 at 19:34):

I need to show that if `i`

is a nonzero even natural number, then there exists some natural number `r`

such that `i = 2*r+2`

. Alas, I cannot for the life of me figure out how to do this; namely I have no idea how to get the (crucial) assumption that `i`

is nonzero into play. Could I get some help?

#### Mario Carneiro (Nov 01 2022 at 19:40):

I assume the word "even" shows up somewhere?

#### Mario Carneiro (Nov 01 2022 at 19:41):

The trick is to get `i = 2*r'`

assuming `i`

is even, and then do `cases`

on `r'`

. If `r' = 0`

then `i`

is zero, which is impossible; and if `r' = r+1`

then `i=2*r+2`

.

#### Connor Gordon (Nov 01 2022 at 19:52):

Yes, I initially left out the word even; I've added it. Supposing I've shown up to r' being nonzero; how to I conclude that it is equal to r+1 for some r?

#### Eric Wieser (Nov 01 2022 at 19:53):

Can you make a #mwe?

#### Eric Wieser (Nov 01 2022 at 19:53):

(bad internet, sorry for the duplicate)

#### Eric Wieser (Nov 01 2022 at 19:53):

(bad internet, sorry for the duplicate)

#### Connor Gordon (Nov 01 2022 at 20:00):

I ended up figuring it out; `cases r'`

does the trick.

Last updated: Dec 20 2023 at 11:08 UTC