Formal target: Corpus.PaperFusibleNumber.conj_7_1

If x is a fusible number and y is its successor, then the interval [x + 1, y + 1) can be divided into intervals [ℓₙ, ℓₙ₊₁), such that the fusible numbers in [ℓₙ, ℓₙ₊₁) are obtained by fusing the n + 1st successor of x with a fusible number.

Exact formal statement

∀ (x y q : Rat) (n : Nat),
  Corpus.PaperFusibleNumber.IsFusible x →
    Corpus.PaperFusibleNumber.IsFusible y →
      LT.lt.{0} x y →
        (∀ (z : Rat), Corpus.PaperFusibleNumber.IsFusible z → Not (Membership.mem.{0, 0} (Set.Ioo.{0} x y) z)) →
          have m := HSub.hSub.{0, 0, 0} y x;
          have ℓ := fun n =>
            HSub.hSub.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} y 1) (HDiv.hDiv.{0, 0, 0} m (HPow.hPow.{0, 0, 0} 2 n));
          Corpus.PaperFusibleNumber.IsFusible q →
            Membership.mem.{0, 0} (Set.Ico.{0} (ℓ n) (ℓ (HAdd.hAdd.{0, 0, 0} n 1))) q →
              Corpus.PaperFusibleNumber.IsFusible
                (HSub.hSub.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 q) 1) x)
                  (HMul.hMul.{0, 0, 0} (HSub.hSub.{0, 0, 0} 2 (HDiv.hDiv.{0, 0, 0} 1 (HPow.hPow.{0, 0, 0} 2 n))) m))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record