mod 2 problem

Stream: new members

[Lucas Allen]

Hi, I want to show that ¬(2 ^ k * a + b) % 2 = 0, given the hypotheses h₀ : 1 ≤ k and ¬b % 2 = 0 or b % 2 = 1. I looked a little in mathlib and tried library_search with no luck. How might I prove this?

[Alex J. Best]

There are some useful lemmas in data.nat.parity so if you import data.nat.parity you can do

open nat

example (k a  b : ℕ) (h₀ : 1 ≤ k) ( hh : b % 2 = 1) : ¬ ((2 ^ k * a + b) % 2 = 0) :=
begin
rw ← not_even_iff at hh,
rw ← even_iff at *,
simp [hh] with parity_simps,
exact or.inl (ne.symm (ne_of_lt h₀)),
end

[Lucas Allen]

Awesome, thank you.

[Kevin Buzzard]

This version avoids the non-terminal simp:

import data.nat.parity
open nat

example (k a  b : ℕ) (h₀ : 1 ≤ k) ( hh : b % 2 = 1) : ¬ ((2 ^ k * a + b) % 2 = 0) :=
begin
  rw ← not_even_iff at hh,
  rw ← even_iff at *,
  suffices : ¬k = 0 ∨ even a,
    simpa [hh] with parity_simps,
  exact or.inl (ne.symm (ne_of_lt h₀)),
end