English
Let a ∈ ℝ and nb ∈ ℕ. If b is the integer −nb and a^(−nb) is a rational number num/den with integers num and den > 0, then a^b is rational with the same representation, i.e. a^b = num/den.
Русский
Пусть a ∈ ℝ и nb ∈ ℕ. Если b является целым числом −nb и a^(−nb) рационально равно num/den (num ∈ ℤ, den ∈ ℕ, den > 0), то a^b рационально и равно num/den.
LaTeX
$$$\text{пусть } a \in \mathbb{R},\ nb \in \mathbb{N},\ num \in \mathbb{Z},\ den \in \mathbb{N}.\quad b = -\text{nb} \ \land \ a^{-\text{nb}} = \dfrac{\text{num}}{\text{den}}\ \Rightarrow\ a^{b} = \dfrac{\text{num}}{\text{den}}.$$$
Lean4
theorem isRat_rpow_neg {a b : ℝ} {nb : ℕ} {num : ℤ} {den : ℕ} (pb : IsInt b (Int.negOfNat nb))
(pe' : IsRat (a ^ (Int.negOfNat nb)) num den) : IsRat (a ^ b) num den := by rwa [pb.out, Real.rpow_intCast]
