English
A variant of the previous lemma for natural exponents, expressing selfZPow of a subtraction of naturals.
Русский
Вариант предыдущего леммa для натуральных степеней, выражающий selfZPow разности натуральных чисел.
LaTeX
$$$selfZPow(x,B,n-m) = mk'(B, x^n, x^m)$ for n,m ∈ N$$
Lean4
@[simp]
theorem selfZPow_add {n m : ℤ} : selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m :=
by
rcases le_or_gt 0 n with hn | hn <;> rcases le_or_gt 0 m with hm | hm
·
rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm, selfZPow_of_nonneg _ _ (add_nonneg hn hm),
Int.natAbs_add_of_nonneg hn hm, pow_add]
· have : n + m = n.natAbs - m.natAbs := by
rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
IsLocalization.mk'_eq_mul_mk'_one, map_pow]
· have : n + m = m.natAbs - n.natAbs := by
rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]
rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]
· rw [selfZPow_of_neg _ _ hn, selfZPow_of_neg _ _ hm, selfZPow_of_neg _ _ (add_neg hn hm),
Int.natAbs_add_of_nonpos hn.le hm.le, ← mk'_mul, one_mul]
congr
ext
simp [pow_add]
