Proof of (-1)^n=... based on n's parity

Stream: new members

[Labyrinth]

Hi, newbie here.

I'm trying to prove that (-1)^n (n is a Nat) is 1 when n is even and -1 when n is odd.
At first I tried to prove each separately by induction, and realised that was harder than I expected when I ran into the output below:

theorem minus_one_power_even (n : Nat) :
  even n → (-1 : Int)^n = 1 := by
  intro he
  induction n with
  | zero => simp
  | succ n' h =>

case succ
n' : ℕ
h : even n' → (-1) ^ n' = 1
he : even (n' + 1)
⊢ (-1) ^ (n' + 1) = 1

Then I thought perhaps trying to prove something like

(even n \-> (-1)^n = 1) \and (odd n \-> (-1)^n = -1)

would work better, but I thought about it more and it seemed like a very clunky way of doing it.

What would be the best way to show what I'm trying to show?

PS: If there's any pre-existing proofs either in the core libraries or in Mathlib that I could use I am also interested in those

[Kenny Lau]

there are a lot of ways to do it, but each way requires you to first set some things up

[Labyrinth]

Correction: It has to be written (-1 : Int) or else I get an error, so the one-liner snippet is incorrect

[Kenny Lau]

i.e. you can't just always use the first tool you have, you need to be clever with your tools

[Eric Wieser]

What is even here? Did you mean docs#Even ?

[Labyrinth]

...Ah! Sorry, I forgot to include my definitions. Here they are:

def even (n : Nat) : Prop := ∃ m, n = 2 * m
def odd (n : Nat)  : Prop := ∃ m, n = 2 * m + 1

I couldn't find anything pre-defined related to even and odd integers online so I started writing my own stuff

[Labyrinth]

I guess I was looking in the wrong places

[Kenny Lau]

then your proof is (-1)^2n = ((-1)^2)^n = 1^n = 1

[Labyrinth]

https://leanprover-community.github.io/mathlib_docs/data/int/parity.html
Welp now I feel even more stupid than that time I posted a question because I didn't include an import Mathlib

[Kenny Lau]

you're on mathlib3

[Kenny Lau]

we've all switched to mathlib4 two years ago

[Labyrinth]

then your proof is (-1)^2n = ((-1)^2)^n = 1^n = 1

Terence Tao was right - I should've tried thinking about the proof first, and only then start to write some Lean4

[Labyrinth]

you're on mathlib3

I didn't think to check the version of the docs I linked to, I just noted how the things I was interested in were already there (which I'm guessing was obvious to you). As far as I know, I'm using mathlib4 though

[Kevin Buzzard]

If your code above compiles, you're using mathlib4 (and lean 4). Your definition of even is not following the capitalisation conventions used in mathlib (terms start with small letters, types start with capitals) and if you'd imported Mathlib and then tried to define Even you would have got an error saying it was defined already, which would have been a good clue.

[Robin Arnez]

This would be the proof with mathlib:

import Mathlib

theorem minus_one_power_even (n : Nat) :
    Even n → (-1 : Int)^n = 1 := by
  intro he
  rw [he.neg_pow, one_pow]

[Kenny Lau]

import Mathlib

theorem minus_one_power_even (n : Nat) :
    Even n → ((-1) ^ n : Int) = 1 := by
  aesop

[Michael Stoll]

import Mathlib.Analysis.Normed.Ring.Lemmas

theorem minus_one_power_even (n : Nat) :
    Even n → (-1 : Int) ^ n = 1 :=
  Even.neg_one_pow

It's actually in the library (found using exact?).

[Notification Bot]

This topic was moved here from #lean4 > Proof of (-1)^n=... based on n's parity by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Labyrinth Please post newbie messages to this channel, not to #lean4.