Mathlib.Algebra.Group.Nat.Even

Nat.even_iff theorem

: Even n ↔ n % 2 = 0

Full source

lemma even_iff : EvenEven n ↔ n % 2 = 0 where
  mp := fun ⟨m, hm⟩ ↦ by simp [← Nat.two_mul, hm]
  mpr h := ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [← Nat.two_mul, h])⟩

Characterization of Even Natural Numbers via Modulo 2

Informal description

A natural number $n$ is even if and only if $n$ modulo 2 equals 0, i.e., $n \equiv 0 \pmod{2}$.

Nat.instDecidablePredEven instance

: DecidablePred (Even : ℕ → Prop)

Full source

instance : DecidablePred (Even : ℕ → Prop) := fun _ ↦ decidable_of_iff _ even_iff.symm

Decidability of Evenness for Natural Numbers

Informal description

For any natural number $n$, the property of being even (i.e., divisible by 2) is decidable.

Nat.instDecidablePredIsSquare instance

: DecidablePred (IsSquare : ℕ → Prop)

Full source

/-- `IsSquare` can be decided on `ℕ` by checking against the square root. -/
instance : DecidablePred (IsSquare : ℕ → Prop) :=
  fun m ↦ decidable_of_iff' (Nat.sqrt m * Nat.sqrt m = m) <| by
    simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]

Decidability of Perfect Squares for Natural Numbers

Informal description

For any natural number $n$, the property of being a perfect square (i.e., there exists a natural number $m$ such that $n = m^2$) is decidable.

Nat.not_even_iff theorem

: ¬Even n ↔ n % 2 = 1

Full source

lemma not_even_iff : ¬ Even n¬ Even n ↔ n % 2 = 1 := by rw [even_iff, mod_two_not_eq_zero]

Characterization of Odd Natural Numbers via Modulo 2

Informal description

A natural number $n$ is not even if and only if $n$ modulo 2 equals 1, i.e., $n \equiv 1 \pmod{2}$.

Nat.two_dvd_ne_zero theorem

: ¬2 ∣ n ↔ n % 2 = 1

Full source

@[simp] lemma two_dvd_ne_zero : ¬2 ∣ n¬2 ∣ n ↔ n % 2 = 1 :=
  (even_iff_exists_two_nsmul _).symm.not.trans not_even_iff

Characterization of Odd Natural Numbers via Divisibility by 2

Informal description

For any natural number $n$, the number $2$ does not divide $n$ if and only if $n$ modulo $2$ equals $1$, i.e., $\neg (2 \mid n) \leftrightarrow n \equiv 1 \pmod{2}$.

Nat.not_even_one theorem

: ¬Even 1

Full source

@[simp] lemma not_even_one : ¬Even 1 := by simp [even_iff]

One is Not Even

Informal description

The natural number $1$ is not even, i.e., $\neg \text{Even}(1)$.

Nat.even_add theorem

: Even (m + n) ↔ (Even m ↔ Even n)

Full source

@[parity_simps] lemma even_add : EvenEven (m + n) ↔ (Even m ↔ Even n) := by
  rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Nat.add_mod]

Parity of Sum: $\text{Even}(m + n) \leftrightarrow (\text{Even}(m) \leftrightarrow \text{Even}(n))$

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ is even if and only if $m$ is even exactly when $n$ is even. In other words, $\text{Even}(m + n) \leftrightarrow (\text{Even}(m) \leftrightarrow \text{Even}(n))$.

Nat.even_add_one theorem

: Even (n + 1) ↔ ¬Even n

Full source

@[parity_simps] lemma even_add_one : EvenEven (n + 1) ↔ ¬Even n := by simp [even_add]

Parity Alternation: $n+1$ is even ↔ $n$ is odd

Informal description

For any natural number $n$, the number $n + 1$ is even if and only if $n$ is not even.

Nat.succ_mod_two_eq_zero_iff theorem

: (m + 1) % 2 = 0 ↔ m % 2 = 1

Full source

lemma succ_mod_two_eq_zero_iff : (m + 1) % 2 = 0 ↔ m % 2 = 1 := by
  simp [← Nat.even_iff, ← Nat.not_even_iff, parity_simps]

Modulo 2 Condition for Successor: $(m + 1) \mod 2 = 0 \leftrightarrow m \mod 2 = 1$

Informal description

For any natural number $m$, the remainder when $m + 1$ is divided by 2 is 0 if and only if the remainder when $m$ is divided by 2 is 1. In other words, $(m + 1) \mod 2 = 0 \leftrightarrow m \mod 2 = 1$.

Nat.succ_mod_two_eq_one_iff theorem

: (m + 1) % 2 = 1 ↔ m % 2 = 0

Full source

lemma succ_mod_two_eq_one_iff : (m + 1) % 2 = 1 ↔ m % 2 = 0 := by
  simp [← Nat.even_iff, ← Nat.not_even_iff, parity_simps]

Modulo 2 Condition for Successor: $(m + 1) \mod 2 = 1 \leftrightarrow m \mod 2 = 0$

Informal description

For any natural number $m$, the remainder when $m + 1$ is divided by 2 is 1 if and only if the remainder when $m$ is divided by 2 is 0. In other words, $(m + 1) \mod 2 = 1 \leftrightarrow m \mod 2 = 0$.

Nat.two_not_dvd_two_mul_add_one theorem

(n : ℕ) : ¬2 ∣ 2 * n + 1

Full source

lemma two_not_dvd_two_mul_add_one (n : ℕ) : ¬2 ∣ 2 * n + 1 := by simp [add_mod]

Odd numbers are not divisible by 2

Informal description

For any natural number $n$, the number $2n + 1$ is not divisible by 2.

Nat.two_not_dvd_two_mul_sub_one theorem

: ∀ {n}, 0 < n → ¬2 ∣ 2 * n - 1

Full source

lemma two_not_dvd_two_mul_sub_one : ∀ {n}, 0 < n → ¬2 ∣ 2 * n - 1
  | n + 1, _ => two_not_dvd_two_mul_add_one n

Odd numbers minus one are not divisible by 2

Informal description

For any positive natural number $n$, the number $2n - 1$ is not divisible by 2.

Nat.even_sub theorem

(h : n ≤ m) : Even (m - n) ↔ (Even m ↔ Even n)

Full source

@[parity_simps] lemma even_sub (h : n ≤ m) : EvenEven (m - n) ↔ (Even m ↔ Even n) := by
  conv_rhs => rw [← Nat.sub_add_cancel h, even_add]
  by_cases h : Even n <;> simp [h]

Parity of Difference: $\text{Even}(m - n) \leftrightarrow (\text{Even}(m) \leftrightarrow \text{Even}(n))$ under $n \leq m$

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, the difference $m - n$ is even if and only if $m$ is even exactly when $n$ is even, i.e., $\text{Even}(m - n) \leftrightarrow (\text{Even}(m) \leftrightarrow \text{Even}(n))$.

Nat.even_mul theorem

: Even (m * n) ↔ Even m ∨ Even n

Full source

@[parity_simps] lemma even_mul : EvenEven (m * n) ↔ Even m ∨ Even n := by
  rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Nat.mul_mod]

Product of Natural Numbers is Even if and Only if One Factor is Even

Informal description

For any natural numbers $m$ and $n$, the product $m \cdot n$ is even if and only if either $m$ is even or $n$ is even.

Nat.even_pow theorem

: Even (m ^ n) ↔ Even m ∧ n ≠ 0

Full source

/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
if and only if `m` is even and `n` is positive. -/
@[parity_simps] lemma even_pow : EvenEven (m ^ n) ↔ Even m ∧ n ≠ 0 := by
  induction n <;> simp +contextual [*, pow_succ', even_mul]

Evenness of Natural Number Powers: $m^n$ is even iff $m$ is even and $n > 0$

Informal description

For any natural numbers $m$ and $n$, the power $m^n$ is even if and only if $m$ is even and $n$ is positive (i.e., $n \neq 0$).

Nat.even_pow' theorem

(h : n ≠ 0) : Even (m ^ n) ↔ Even m

Full source

lemma even_pow' (h : n ≠ 0) : EvenEven (m ^ n) ↔ Even m := even_pow.trans <| and_iff_left h

Evenness of Nonzero Powers: $m^n$ is even iff $m$ is even for $n > 0$

Informal description

For any natural numbers $m$ and $n$ with $n \neq 0$, the power $m^n$ is even if and only if $m$ is even.

Nat.even_mul_succ_self theorem

(n : ℕ) : Even (n * (n + 1))

Full source

lemma even_mul_succ_self (n : ℕ) : Even (n * (n + 1)) := by rw [even_mul, even_add_one]; exact em _

Product of Consecutive Natural Numbers is Even

Informal description

For any natural number $n$, the product $n \cdot (n + 1)$ is even.

Nat.even_mul_pred_self theorem

: ∀ n : ℕ, Even (n * (n - 1))

Full source

lemma even_mul_pred_self : ∀ n : ℕ, Even (n * (n - 1))
  | 0 => .zero
  | (n + 1) => mul_comm (n + 1 - 1) (n + 1) ▸ even_mul_succ_self n

Product of a Natural Number and Its Predecessor is Even

Informal description

For any natural number $n$, the product $n \cdot (n - 1)$ is even.

Nat.two_mul_div_two_of_even theorem

: Even n → 2 * (n / 2) = n

Full source

lemma two_mul_div_two_of_even : Even n → 2 * (n / 2) = n := fun h ↦
  Nat.mul_div_cancel_left' ((even_iff_exists_two_nsmul _).1 h)

Double of Half of Even Natural Number Equals Itself

Informal description

For any even natural number $n$, it holds that $2 \cdot (n / 2) = n$.

Nat.div_two_mul_two_of_even theorem

: Even n → n / 2 * 2 = n

Full source

lemma div_two_mul_two_of_even : Even n → n / 2 * 2 = n :=
  fun h ↦ Nat.div_mul_cancel ((even_iff_exists_two_nsmul _).1 h)

Division-Multiplication Identity for Even Natural Numbers

Informal description

For any even natural number $n$, the product of $n/2$ and $2$ equals $n$, i.e., $\frac{n}{2} \times 2 = n$.

Nat.one_lt_of_ne_zero_of_even theorem

(h0 : n ≠ 0) (hn : Even n) : 1 < n

Full source

theorem one_lt_of_ne_zero_of_even (h0 : n ≠ 0) (hn : Even n) : 1 < n := by
  refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr (And.intro h0 ?_)
  intro h
  rw [h] at hn
  exact Nat.not_even_one hn

Nonzero Even Natural Numbers Are Greater Than One

Informal description

For any natural number $n$ such that $n \neq 0$ and $n$ is even, it follows that $1 < n$.

Nat.add_one_lt_of_even theorem

(hn : Even n) (hm : Even m) (hnm : n < m) : n + 1 < m

Full source

theorem add_one_lt_of_even (hn : Even n) (hm : Even m) (hnm : n < m) :
    n + 1 < m := by
  rcases hn with ⟨n, rfl⟩
  rcases hm with ⟨m, rfl⟩
  omega

Strict Inequality Preservation for Successor of Even Natural Numbers

Informal description

For any even natural numbers $n$ and $m$ such that $n < m$, it follows that $n + 1 < m$.