The Distinct Prime Factor Count Bound

Abstract

A nonzero integer has at most its floor base-two logarithm many distinct prime factors.

Theorem 1.1 (Distinct prime factors obey a floor logarithmic bound).

$$d\ne 0\Rightarrow \left(2^{\mathrm{omega}\left(|d|\right)}\le \mathrm{distinctPrimeProduct}\left(\left|d\right|\right)\wedge \left(\mathrm{distinctPrimeProduct}\left(\left|d\right|\right)\le \left|d\right|\wedge \mathrm{omega}\left(\left|d\right|\right)\le floorLog2\left(\left|d\right|\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/PrimeProducts/DistinctPrimeFactorCountBound.distinct_prime_factor_count_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let d be nonzero. Every prime divisor of its absolute value is at least two, so their product is at least two raised to the number of distinct prime divisors.

The product of the distinct prime divisors is the natural-number radical of the absolute value. The radical divides a nonzero natural number and is therefore at most that number.

Combining the two inequalities and applying the defining adjunction for the natural floor logarithm gives the stated base-two bound.

References

• Truth anchor: D5/S3/Analytic/PrimeProducts/DistinctPrimeFactorCountBound.distinct_prime_factor_count_bound