English
For every integer m, preNormEDS(b,c,d)(2m) equals preNormEDS(b,c,d)(m−1)^2 · preNormEDS(b,c,d)(m) · preNormEDS(b,c,d)(m+2) − preNormEDS(b,c,d)(m−2) · preNormEDS(b,c,d)(m) · preNormEDS(b,c,d)(m+1)^2.
Русский
Для целого m выполняется: preNormEDS(b,c,d)(2m) = preNormEDS(b,c,d)(m−1)^2 · preNormEDS(b,c,d)(m) · preNormEDS(b,c,d)(m+2) − preNormEDS(b,c,d)(m−2) · preNormEDS(b,c,d)(m) · preNormEDS(b,c,d)(m+1)^2.
LaTeX
$$$$\text{preNormEDS}(b,c,d,2m) = \text{preNormEDS}(b,c,d,m-1)^2 \cdot \text{preNormEDS}(b,c,d,m) \cdot \text{preNormEDS}(b,c,d,m+2) \\ - \text{preNormEDS}(b,c,d,m-2) \cdot \text{preNormEDS}(b,c,d,m) \cdot \text{preNormEDS}(b,c,d,m+1)^2.$$$$
Lean4
theorem preNormEDS_even (m : ℤ) :
preNormEDS b c d (2 * m) =
preNormEDS b c d (m - 1) ^ 2 * preNormEDS b c d m * preNormEDS b c d (m + 2) -
preNormEDS b c d (m - 2) * preNormEDS b c d m * preNormEDS b c d (m + 1) ^ 2 :=
by
induction m using Int.negInduction with
| nat m =>
rcases m with _ | _ | _ | m
iterate 3 simp
simp_rw [Nat.cast_succ, Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl, Int.add_sub_cancel]
norm_cast
simpa only [preNormEDS_ofNat] using preNormEDS'_even ..
| neg ih m =>
simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]
ring1
