zpow_neg_iff — Mathlib

English

If n is odd, then a^n < 0 iff a < 0.

Русский

Если n нечетно, то a^n < 0 тогда и только тогда a < 0.

LaTeX

$$$\\text{Odd}(n) \\Rightarrow (a^{n} < 0 \\iff a < 0)$$$

Lean4

theorem zpow_neg_iff (hn : Odd n) : a ^ n < 0 ↔ a < 0 :=
  by
  refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add_one₀ ha.ne]
  exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

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