English
If a ≠ 0 and a ≠ ∞, then for every integer n, a^n > 0.
Русский
Если a ≠ 0 и a ≠ ∞, то для любого целого n имеем a^n > 0.
LaTeX
$$$\\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\ a \\neq 0 \\land a \\neq \\infty \\Rightarrow \\forall n \\in \\mathbb{Z}, 0 < a^n$$$
Lean4
theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n :=
by
cases n
· simpa using ENNReal.pow_pos ha.bot_lt _
· simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and, not_false_eq_true]