abundant_iff_not_perfect_and_not_deficient

English

Let n ≠ 0. Then Abundant n iff not Perfect n and not Deficient n.

Русский

Пусть n ≠ 0. Тогда n избыточно тогда и только тогда, когда n не является ни совершенным, ни дефицитным.

LaTeX

$$$n \neq 0 \Rightarrow \operatorname{Abundant}(n) \iff (\lnot \operatorname{Perfect}(n) \land \lnot \operatorname{Deficient}(n))$$$

Lean4

theorem abundant_iff_not_perfect_and_not_deficient (hn : 0 ≠ n) : Abundant n ↔ ¬Perfect n ∧ ¬Deficient n :=
  by
  dsimp only [Perfect, Abundant, Deficient]
  cutsat

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