Lemma: Agent20_CollatzPartial_01a13459_E20.growth_in_same_residue

For every positive natural modulus M, there is n>1 with n<U(n) and n mod M=U(n) mod M.

Exact formal statement

∀ (M : Nat),
  LT.lt.{0} 0 M →
    Exists.{1} fun n =>
      And (LT.lt.{0} 1 n)
        (And (LT.lt.{0} n (Agent20_CollatzPartial_01a13459_E20.U n))
          (Eq.{1} (HMod.hMod.{0, 0, 0} n M) (HMod.hMod.{0, 0, 0} (Agent20_CollatzPartial_01a13459_E20.U n) M)))

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

Environment availability: available.

Public JSON record