Lemma: Agent20_CollatzRound2_01a13459_E20_V2.multiple_three_backward_tree

For all natural n,k, if U^k(n) is divisible by 3, then n=2^k*U^k(n). This describes all genuine predecessors of multiples of three.

Exact formal statement

∀ (n k : Nat),
  Eq.{1} (HMod.hMod.{0, 0, 0} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter n k) 3) 0 →
    Eq.{1} n (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter n k))

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record