Quint sublist inclusion and quintic factor evaluation

Proved

Erdos390.tail_divisor_quint_sublist

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsorder-theory

Let $L$ be a strictly ascending list of natural numbers (L.Pairwise (· < ·)), and let $a, b, c, d, e \in \mathbb{N}$ satisfy $a, b, c, d, e \in L$ and $a < b < c < d < e$ . Then the five-element list $[a, b, c, d, e]$ is a sublist of $L$ (List.Sublist [a, b, c, d, e] L), and its product is $a \cdot b \cdot c \cdot d \cdot e$ (List.prod [a, b, c, d, e] = a * b * c * d * e).

Preamble

import Mathlib.Data.List.Basic
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_quint_sublist
    {L : List ℕ} {a b c d e : ℕ}
    (hL : L.Pairwise (· < ·))
    (ha : a ∈ L) (hb : b ∈ L) (hc : c ∈ L) (hd : d ∈ L) (he : e ∈ L)
    (hab : a < b) (hbc : b < c) (hcd : c < d) (hde : d < e) :
    List.Sublist [a, b, c, d, e] L ∧ List.prod [a, b, c, d, e] = a * b * c * d * e := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.Sublist constructors

View graph