int_prod_range_pos — Mathlib

English

If n is even and m is outside the interval [0,n), then 0 < ∏_{k=0}^{n-1} (m - k).

Русский

Если n чётно и m выходит за интервал [0,n), то произведение положительно.

LaTeX

$$(Even n) ∧ (m ∉ Ico 0 n) ⇒ 0 < ∏_{k ∈ range n} (m - k)$$

Lean4

theorem int_prod_range_pos {m : ℤ} {n : ℕ} (hn : Even n) (hm : m ∉ Ico (0 : ℤ) n) : 0 < ∏ k ∈ Finset.range n, (m - k) :=
  by
  refine (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm ?_
  rw [eq_comm, Finset.prod_eq_zero_iff] at h
  obtain ⟨a, ha, h⟩ := h
  rw [sub_eq_zero.1 h]
  exact ⟨Int.ofNat_zero_le _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩

Похожие утверждения