silly computation with even numbers

Stream: new members

[Connor Gordon]

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]

I assume the word "even" shows up somewhere?

[Mario Carneiro]

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]

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]

Can you make a #mwe?

[Eric Wieser]

(bad internet, sorry for the duplicate)

[Eric Wieser]

(bad internet, sorry for the duplicate)

[Connor Gordon]

I ended up figuring it out; cases r' does the trick.