English
If n is a composite natural number, then the square of its smallest prime factor is at most n.
Русский
Пусть n — составное натуральное число. Тогда квадрат наименьшего простого делителя n не превышает n.
LaTeX
$$$\\\\forall n \\, (0 < n \land \neg \\\\mathrm{Prime}(n)) \\\\Rightarrow (\\\\minFac n)^2 \\\\le n$$$
Lean4
/-- The square of the smallest prime factor of a composite number `n` is at most `n`.
-/
theorem minFac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬Prime n) : minFac n ^ 2 ≤ n :=
have t : minFac n ≤ n / minFac n := minFac_le_div w h
calc
minFac n ^ 2 = minFac n * minFac n := sq (minFac n)
_ ≤ n / minFac n * minFac n := (Nat.mul_le_mul_right (minFac n) t)
_ ≤ n := div_mul_le_self n (minFac n)
