Ordered extraction of four prime support elements

Proved

OddPerfectNumber.four_support_ordered

by WillR · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-supportodd-perfectorderingprimefactors

A natural number with exactly four distinct prime divisors has those divisors represented by four strictly increasing primes.

Preamble

import Mathlib

Formal statement

theorem OddPerfectNumber.four_support_ordered (m : Nat)
    (hcard : m.primeFactors.card = 4) :
    ∃ q1 q2 q3 q4 : Nat,
      q1.Prime ∧ q2.Prime ∧ q3.Prime ∧ q4.Prime ∧
      q1 < q2 ∧ q2 < q3 ∧ q3 < q4 ∧
      m.primeFactors = {q1, q2, q3, q4} := by sorry

View graph