FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Data.Nat.PrimeFin
public import Mathlib.Order.Lattice.Nat

@[expose] public sectionnamespace Nat

The greatest prime divisor of a natural number n > 1.

Takes the junk value 0 for n = 0 and 1 for n = 1.

def maxPrimeFac (n : ℕ) : ℕ := if n = 1 then 1 else n.primeFactorsList.getLastIexample : maxPrimeFac 0 = 0 := by⊢ maxPrimeFac 0 = 0 decide +kernelAll goals completed! 🐙example : maxPrimeFac 1 = 1 := rflexample : maxPrimeFac 12 = 3 := by⊢ maxPrimeFac 12 = 3 decide +kernelAll goals completed! 🐙example : maxPrimeFac 97 = 97 := by⊢ maxPrimeFac 97 = 97 decide +kernelAll goals completed! 🐙example : maxPrimeFac 125 = 5 := by⊢ maxPrimeFac 125 = 5 decide +kernelAll goals completed! 🐙example : maxPrimeFac 360 = 5 := by⊢ maxPrimeFac 360 = 5 decide +kernelAll goals completed! 🐙

@[simp]
lemma maxPrimeFac_zero :
    maxPrimeFac 0 = 0 := by⊢ maxPrimeFac 0 = 0
  simp [maxPrimeFac, List.getLastI]All goals completed! 🐙

@[simp]
lemma maxPrimeFac_one :
    maxPrimeFac 1 = 1 := rfl

lemma prime_maxPrimeFac_of_one_lt (n : ℕ) (h : 1 < n) :
    Prime (maxPrimeFac n) := byn:ℕh:1 < n⊢ Prime n.maxPrimeFac
  have hn : n.primeFactorsList ≠ [] := (primeFactorsList_ne_nil n).2 hn:ℕh:1 < nhn:n.primeFactorsList ≠ []⊢ Prime n.maxPrimeFac
  have hmem : n.primeFactorsList.getLast hn ∈ n.primeFactorsList := List.getLast_mem hnn:ℕh:1 < nhn:n.primeFactorsList ≠ []hmem:n.primeFactorsList.getLast hn ∈ n.primeFactorsList⊢ Prime n.maxPrimeFac
  have hprime : Prime (n.primeFactorsList.getLast hn) := prime_of_mem_primeFactorsList hmemn:ℕh:1 < nhn:n.primeFactorsList ≠ []hmem:n.primeFactorsList.getLast hn ∈ n.primeFactorsListhprime:Prime (n.primeFactorsList.getLast hn)⊢ Prime n.maxPrimeFac
  simpa [maxPrimeFac, h.ne', List.getLastI_eq_getLast?_getD,
    List.getLast?_eq_getLast_of_ne_nil hn] using hprimeAll goals completed! 🐙

The greatest prime factor of a natural number divides it.


lemma maxPrimeFac_dvd : ∀ {n : ℕ}, maxPrimeFac n ∣ n
  | 0 =>⊢ maxPrimeFac 0 ∣ 0 by⊢ maxPrimeFac 0 ∣ 0 simpAll goals completed! 🐙
  | 1 =>⊢ maxPrimeFac 1 ∣ 1 by⊢ maxPrimeFac 1 ∣ 1 simpAll goals completed! 🐙
  | n + 2 =>n:ℕ⊢ (n + 2).maxPrimeFac ∣ n + 2 byn:ℕ⊢ (n + 2).maxPrimeFac ∣ n + 2
    have hn : 1 < n + 2 := by omegan:ℕhn:1 < n + 2⊢ (n + 2).maxPrimeFac ∣ n + 2n:ℕhn:1 < n + 2⊢ (n + 2).maxPrimeFac ∣ n + 2
    have hlist : (n + 2).primeFactorsList ≠ [] :=
      (primeFactorsList_ne_nil (n + 2)).2 hnn:ℕhn:1 < n + 2hlist:(n + 2).primeFactorsList ≠ []⊢ (n + 2).maxPrimeFac ∣ n + 2
    have hmem : (n + 2).primeFactorsList.getLast hlist ∈ (n + 2).primeFactorsList :=
      List.getLast_mem hlistn:ℕhn:1 < n + 2hlist:(n + 2).primeFactorsList ≠ []hmem:(n + 2).primeFactorsList.getLast hlist ∈ (n + 2).primeFactorsList⊢ (n + 2).maxPrimeFac ∣ n + 2
    have hdvd : (n + 2).primeFactorsList.getLast hlist ∣ n + 2 :=
      dvd_of_mem_primeFactorsList hmemn:ℕhn:1 < n + 2hlist:(n + 2).primeFactorsList ≠ []hmem:(n + 2).primeFactorsList.getLast hlist ∈ (n + 2).primeFactorsListhdvd:(n + 2).primeFactorsList.getLast hlist ∣ n + 2⊢ (n + 2).maxPrimeFac ∣ n + 2
    simpa [maxPrimeFac, hn.ne', List.getLastI_eq_getLast?_getD,
      List.getLast?_eq_getLast_of_ne_nil hlist] using hdvdAll goals completed! 🐙

Every prime factor of a nonzero natural number is at most its greatest prime factor.

lemma le_maxPrimeFac
    {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) (h_dvd : p ∣ n) :
    p ≤ maxPrimeFac n := byn:ℕp:ℕhn:n ≠ 0hp:Prime ph_dvd:p ∣ n⊢ p ≤ n.maxPrimeFac
  have hmem : p ∈ n.primeFactorsList := (mem_primeFactorsList hn).2 ⟨hp, h_dvd⟩n:ℕp:ℕhn:n ≠ 0hp:Prime ph_dvd:p ∣ nhmem:p ∈ n.primeFactorsList⊢ p ≤ n.maxPrimeFac
  have hlist : n.primeFactorsList ≠ [] := List.ne_nil_of_mem hmemn:ℕp:ℕhn:n ≠ 0hp:Prime ph_dvd:p ∣ nhmem:p ∈ n.primeFactorsListhlist:n.primeFactorsList ≠ []⊢ p ≤ n.maxPrimeFac
  have hn_one : n ≠ 1 := ((primeFactorsList_ne_nil n).1 hlist).ne'n:ℕp:ℕhn:n ≠ 0hp:Prime ph_dvd:p ∣ nhmem:p ∈ n.primeFactorsListhlist:n.primeFactorsList ≠ []hn_one:n ≠ 1⊢ p ≤ n.maxPrimeFac
  have hp_last : p ≤ n.primeFactorsList.getLast hlist :=
    (primeFactorsList_sorted n).pairwise.rel_getLast hmemn:ℕp:ℕhn:n ≠ 0hp:Prime ph_dvd:p ∣ nhmem:p ∈ n.primeFactorsListhlist:n.primeFactorsList ≠ []hn_one:n ≠ 1hp_last:p ≤ n.primeFactorsList.getLast hlist⊢ p ≤ n.maxPrimeFac
  simpa [maxPrimeFac, hn_one, List.getLastI_eq_getLast?_getD,
    List.getLast?_eq_getLast_of_ne_nil hlist] using hp_lastAll goals completed! 🐙

lemma maxPrimeFac_eq_of_dvd_of_le
    (n p : ℕ) (hn : 0 < n) (hp : p.Prime) (h_dvd : p ∣ n) (h_le : maxPrimeFac n ≤ p) :
    maxPrimeFac n = p := byn:ℕp:ℕhn:0 < nhp:Prime ph_dvd:p ∣ nh_le:n.maxPrimeFac ≤ p⊢ n.maxPrimeFac = p
  exact le_antisymm h_le (le_maxPrimeFac hn.ne' hp h_dvd)All goals completed! 🐙

The greatest prime factor of a prime is the prime itself.

@[simp]
lemma Prime.maxPrimeFac_eq_self {p : ℕ} (hp : p.Prime) :
    maxPrimeFac p = p := byp:ℕhp:Prime p⊢ p.maxPrimeFac = p
  apply maxPrimeFac_eq_of_dvd_of_le p p hp.pos hp (dvd_refl p)p:ℕhp:Prime p⊢ p.maxPrimeFac ≤ p
  exact Nat.le_of_dvd hp.pos maxPrimeFac_dvdAll goals completed! 🐙

The fixed points of maxPrimeFac are zero, one, and the primes.

@[simp]
lemma maxPrimeFac_eq_self_iff {n : ℕ} :
    maxPrimeFac n = n ↔ n ≤ 1 ∨ n.Prime := byn:ℕ⊢ n.maxPrimeFac = n ↔ n ≤ 1 ∨ Prime n
  constructormpn:ℕ⊢ n.maxPrimeFac = n → n ≤ 1 ∨ Prime nmprn:ℕ⊢ n ≤ 1 ∨ Prime n → n.maxPrimeFac = n
  ·mpn:ℕ⊢ n.maxPrimeFac = n → n ≤ 1 ∨ Prime n intro hmpn:ℕh:n.maxPrimeFac = n⊢ n ≤ 1 ∨ Prime n
    by_cases hn : n ≤ 1posn:ℕh:n.maxPrimeFac = nhn:n ≤ 1⊢ n ≤ 1 ∨ Prime nnegn:ℕh:n.maxPrimeFac = nhn:¬n ≤ 1⊢ n ≤ 1 ∨ Prime n
    ·posn:ℕh:n.maxPrimeFac = nhn:n ≤ 1⊢ n ≤ 1 ∨ Prime n exact Or.inl hnAll goals completed! 🐙
    ·negn:ℕh:n.maxPrimeFac = nhn:¬n ≤ 1⊢ n ≤ 1 ∨ Prime n exact Or.inr <| h ▸ prime_maxPrimeFac_of_one_lt n (lt_of_not_ge hn)All goals completed! 🐙
  ·mprn:ℕ⊢ n ≤ 1 ∨ Prime n → n.maxPrimeFac = n rintro (hn | hn)mpr.inln:ℕhn:n ≤ 1⊢ n.maxPrimeFac = nmpr.inrn:ℕhn:Prime n⊢ n.maxPrimeFac = n
    ·mpr.inln:ℕhn:n ≤ 1⊢ n.maxPrimeFac = n obtain rfl | rfl := Nat.le_one_iff_eq_zero_or_eq_one.mp hnmpr.inl.inlhn:0 ≤ 1⊢ maxPrimeFac 0 = 0mpr.inl.inrhn:1 ≤ 1⊢ maxPrimeFac 1 = 1 <;>mpr.inl.inlhn:0 ≤ 1⊢ maxPrimeFac 0 = 0mpr.inl.inrhn:1 ≤ 1⊢ maxPrimeFac 1 = 1 simpAll goals completed! 🐙
    ·mpr.inrn:ℕhn:Prime n⊢ n.maxPrimeFac = n exact hn.maxPrimeFac_eq_selfAll goals completed! 🐙

The greatest prime factor of a product of nonzero natural numbers is the maximum of their greatest prime factors.


lemma maxPrimeFac_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
    maxPrimeFac (m * n) = max (maxPrimeFac m) (maxPrimeFac n) := bym:ℕn:ℕhm:m ≠ 0hn:n ≠ 0⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac
  obtain rfl | hm_lt : m = 1 ∨ 1 < m := bym:ℕn:ℕhm:m ≠ 0hn:n ≠ 0⊢ m = 1 ∨ 1 < minln:ℕhn:n ≠ 0hm:1 ≠ 0⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFacinrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < m⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac omegainln:ℕhn:n ≠ 0hm:1 ≠ 0⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFacinrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < m⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFacinrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < m⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac
  ·inln:ℕhn:n ≠ 0hm:1 ≠ 0⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac have hle : 1 ≤ maxPrimeFac n := bym:ℕn:ℕhm:m ≠ 0hn:n ≠ 0⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac
      obtain rfl | hn_lt : n = 1 ∨ 1 < n := byn:ℕhn:n ≠ 0hm:1 ≠ 0⊢ n = 1 ∨ 1 < ninlhm:1 ≠ 0hn:1 ≠ 0⊢ 1 ≤ maxPrimeFac 1inrn:ℕhn:n ≠ 0hm:1 ≠ 0hn_lt:1 < n⊢ 1 ≤ n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac omegainlhm:1 ≠ 0hn:1 ≠ 0⊢ 1 ≤ maxPrimeFac 1inrn:ℕhn:n ≠ 0hm:1 ≠ 0hn_lt:1 < n⊢ 1 ≤ n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFacinlhm:1 ≠ 0hn:1 ≠ 0⊢ 1 ≤ maxPrimeFac 1inrn:ℕhn:n ≠ 0hm:1 ≠ 0hn_lt:1 < n⊢ 1 ≤ n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac
      ·inlhm:1 ≠ 0hn:1 ≠ 0⊢ 1 ≤ maxPrimeFac 1inln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac simpAll goals completed! 🐙inln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac
      ·inrn:ℕhn:n ≠ 0hm:1 ≠ 0hn_lt:1 < n⊢ 1 ≤ n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac exact (prime_maxPrimeFac_of_one_lt n hn_lt).one_lt.leinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFacinln:ℕhn:n ≠ 0hm:1 ≠ 0hle:1 ≤ n.maxPrimeFac⊢ (1 * n).maxPrimeFac = max (maxPrimeFac 1) n.maxPrimeFac
    simp [hle]All goals completed! 🐙
  obtain rfl | hn_lt : n = 1 ∨ 1 < n := bym:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < m⊢ n = 1 ∨ 1 < ninr.inlm:ℕhm:m ≠ 0hm_lt:1 < mhn:1 ≠ 0⊢ (m * 1).maxPrimeFac = max m.maxPrimeFac (maxPrimeFac 1)inr.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < n⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac omegainr.inlm:ℕhm:m ≠ 0hm_lt:1 < mhn:1 ≠ 0⊢ (m * 1).maxPrimeFac = max m.maxPrimeFac (maxPrimeFac 1)inr.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < n⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFacinr.inlm:ℕhm:m ≠ 0hm_lt:1 < mhn:1 ≠ 0⊢ (m * 1).maxPrimeFac = max m.maxPrimeFac (maxPrimeFac 1)inr.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < n⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac
  ·inr.inlm:ℕhm:m ≠ 0hm_lt:1 < mhn:1 ≠ 0⊢ (m * 1).maxPrimeFac = max m.maxPrimeFac (maxPrimeFac 1) have hle : 1 ≤ maxPrimeFac m := (prime_maxPrimeFac_of_one_lt m hm_lt).one_lt.leinr.inlm:ℕhm:m ≠ 0hm_lt:1 < mhn:1 ≠ 0hle:1 ≤ m.maxPrimeFac⊢ (m * 1).maxPrimeFac = max m.maxPrimeFac (maxPrimeFac 1)
    simp [hle]All goals completed! 🐙
  have hmn_lt : 1 < m * n := Nat.one_lt_mul_iff.mpr
    ⟨zero_lt_of_lt hm_lt, zero_lt_of_lt hn_lt, Or.inl hm_lt⟩inr.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac
  apply le_antisymminr.inr.am:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFacam:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ max m.maxPrimeFac n.maxPrimeFac ≤ (m * n).maxPrimeFac
  ·inr.inr.am:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFac have hp : Prime (maxPrimeFac (m * n)) := prime_maxPrimeFac_of_one_lt (m * n) hmn_ltinr.inr.am:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime (m * n).maxPrimeFac⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFac
    rcases hp.dvd_mul.mp maxPrimeFac_dvd with hpm | hpninr.inr.a.inlm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime (m * n).maxPrimeFachpm:(m * n).maxPrimeFac ∣ m⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFacinr.inr.a.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime (m * n).maxPrimeFachpn:(m * n).maxPrimeFac ∣ n⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFac
    ·inr.inr.a.inlm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime (m * n).maxPrimeFachpm:(m * n).maxPrimeFac ∣ m⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFac exact (le_maxPrimeFac hm hp hpm).trans (le_max_left _ _)All goals completed! 🐙
    ·inr.inr.a.inrm:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime (m * n).maxPrimeFachpn:(m * n).maxPrimeFac ∣ n⊢ (m * n).maxPrimeFac ≤ max m.maxPrimeFac n.maxPrimeFac exact (le_maxPrimeFac hn hp hpn).trans (le_max_right _ _)All goals completed! 🐙
  ·am:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ max m.maxPrimeFac n.maxPrimeFac ≤ (m * n).maxPrimeFac apply max_lea.h₁m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ m.maxPrimeFac ≤ (m * n).maxPrimeFach₂m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ n.maxPrimeFac ≤ (m * n).maxPrimeFac
    ·a.h₁m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ m.maxPrimeFac ≤ (m * n).maxPrimeFac have hp : Prime (maxPrimeFac m) := prime_maxPrimeFac_of_one_lt m hm_lta.h₁m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime m.maxPrimeFac⊢ m.maxPrimeFac ≤ (m * n).maxPrimeFac
      apply le_maxPrimeFac (mul_ne_zero hm hn) hpa.h₁m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime m.maxPrimeFac⊢ m.maxPrimeFac ∣ m * n
      exact dvd_mul_of_dvd_left maxPrimeFac_dvd nAll goals completed! 🐙
    ·h₂m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * n⊢ n.maxPrimeFac ≤ (m * n).maxPrimeFac have hp : Prime (maxPrimeFac n) := prime_maxPrimeFac_of_one_lt n hn_lth₂m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime n.maxPrimeFac⊢ n.maxPrimeFac ≤ (m * n).maxPrimeFac
      apply le_maxPrimeFac (mul_ne_zero hm hn) hph₂m:ℕn:ℕhm:m ≠ 0hn:n ≠ 0hm_lt:1 < mhn_lt:1 < nhmn_lt:1 < m * nhp:Prime n.maxPrimeFac⊢ n.maxPrimeFac ∣ m * n
      exact dvd_mul_of_dvd_right maxPrimeFac_dvd mAll goals completed! 🐙

The greatest prime factor of a nonzero power is the greatest prime factor of its base.


@[simp]
lemma maxPrimeFac_pow {k : ℕ} (hk : k ≠ 0) (n : ℕ) :
    maxPrimeFac (n ^ k) = maxPrimeFac n :=
  match k, hk with
  | k + 1, _ =>k✝:ℕhk:k✝ ≠ 0n:ℕk:ℕx✝:k + 1 ≠ 0⊢ (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFac byk✝:ℕhk:k✝ ≠ 0n:ℕk:ℕx✝:k + 1 ≠ 0⊢ (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFac
    by_cases hn : n = 0posk✝:ℕhk:k✝ ≠ 0n:ℕk:ℕx✝:k + 1 ≠ 0hn:n = 0⊢ (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacnegk✝:ℕhk:k✝ ≠ 0n:ℕk:ℕx✝:k + 1 ≠ 0hn:¬n = 0⊢ (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFac
    ·posk✝:ℕhk:k✝ ≠ 0n:ℕk:ℕx✝:k + 1 ≠ 0hn:n = 0⊢ (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFac subst nposk✝:ℕhk:k✝ ≠ 0k:ℕx✝:k + 1 ≠ 0⊢ (0 ^ (k + 1)).maxPrimeFac = maxPrimeFac 0
      simpAll goals completed! 🐙
    induction k with
    | zero =>neg.zerok:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0x✝:0 + 1 ≠ 0⊢ (n ^ (0 + 1)).maxPrimeFac = n.maxPrimeFac simpAll goals completed! 🐙
    | succ k ih =>neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ (n ^ (k + 1 + 1)).maxPrimeFac = n.maxPrimeFac
        rw [pow_succ,neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ (n ^ (k + 1) * n).maxPrimeFac = n.maxPrimeFacneg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max n.maxPrimeFac n.maxPrimeFac = n.maxPrimeFac maxPrimeFac_mul (pow_ne_zero _ hn) hn,neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max (n ^ (k + 1)).maxPrimeFac n.maxPrimeFac = n.maxPrimeFacneg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max n.maxPrimeFac n.maxPrimeFac = n.maxPrimeFac ih (byk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ k + 1 ≠ 0neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max n.maxPrimeFac n.maxPrimeFac = n.maxPrimeFac omegaAll goals completed! 🐙neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max n.maxPrimeFac n.maxPrimeFac = n.maxPrimeFac)]neg.succk✝:ℕhk:k✝ ≠ 0n:ℕhn:¬n = 0k:ℕih:k + 1 ≠ 0 → (n ^ (k + 1)).maxPrimeFac = n.maxPrimeFacx✝:k + 1 + 1 ≠ 0⊢ max n.maxPrimeFac n.maxPrimeFac = n.maxPrimeFac
        simpAll goals completed! 🐙

The greatest prime factor of a natural number is at most that number.

lemma maxPrimeFac_le : ∀ {n : ℕ}, maxPrimeFac n ≤ n
  | 0 =>⊢ maxPrimeFac 0 ≤ 0 by⊢ maxPrimeFac 0 ≤ 0 simpAll goals completed! 🐙
  | 1 =>⊢ maxPrimeFac 1 ≤ 1 by⊢ maxPrimeFac 1 ≤ 1 simpAll goals completed! 🐙
  | n + 2 => Nat.le_of_dvd (byn:ℕ⊢ 0 < n + 2 omegaAll goals completed! 🐙) maxPrimeFac_dvd

The greatest prime factor of a natural number greater than one is the least upper bound of its prime factors.

lemma isLeast_maxPrimeFac {n : ℕ} (hn : 1 < n) :
    IsLeast (upperBounds {p : ℕ | p.Prime ∧ p ∣ n}) (maxPrimeFac n) := byn:ℕhn:1 < n⊢ IsLeast (upperBounds {p | Prime p ∧ p ∣ n}) n.maxPrimeFac
  constructorleftn:ℕhn:1 < n⊢ n.maxPrimeFac ∈ upperBounds {p | Prime p ∧ p ∣ n}rightn:ℕhn:1 < n⊢ n.maxPrimeFac ∈ lowerBounds (upperBounds {p | Prime p ∧ p ∣ n})
  ·leftn:ℕhn:1 < n⊢ n.maxPrimeFac ∈ upperBounds {p | Prime p ∧ p ∣ n} rintro p ⟨hp, h_dvd⟩leftn:ℕhn:1 < np:ℕhp:Prime ph_dvd:p ∣ n⊢ p ≤ n.maxPrimeFac
    exact le_maxPrimeFac (zero_lt_of_lt hn).ne' hp h_dvdAll goals completed! 🐙
  ·rightn:ℕhn:1 < n⊢ n.maxPrimeFac ∈ lowerBounds (upperBounds {p | Prime p ∧ p ∣ n}) intro b hbrightn:ℕhn:1 < nb:ℕhb:b ∈ upperBounds {p | Prime p ∧ p ∣ n}⊢ n.maxPrimeFac ≤ b
    exact hb ⟨prime_maxPrimeFac_of_one_lt n hn, maxPrimeFac_dvd⟩All goals completed! 🐙

Away from n = 1, the computable greatest prime factor agrees with its supremum characterization.


lemma maxPrimeFac_eq_sSup {n : ℕ} (hn_one : n ≠ 1) :
    maxPrimeFac n = sSup {p : ℕ | p.Prime ∧ p ∣ n} := byn:ℕhn_one:n ≠ 1⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n}
  obtain rfl | hn : n = 0 ∨ 1 < n := byn:ℕhn_one:n ≠ 1⊢ n = 0 ∨ 1 < ninlhn_one:0 ≠ 1⊢ maxPrimeFac 0 = sSup {p | Prime p ∧ p ∣ 0}inrn:ℕhn_one:n ≠ 1hn:1 < n⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n} liainlhn_one:0 ≠ 1⊢ maxPrimeFac 0 = sSup {p | Prime p ∧ p ∣ 0}inrn:ℕhn_one:n ≠ 1hn:1 < n⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n}inlhn_one:0 ≠ 1⊢ maxPrimeFac 0 = sSup {p | Prime p ∧ p ∣ 0}inrn:ℕhn_one:n ≠ 1hn:1 < n⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n}
  ·inlhn_one:0 ≠ 1⊢ maxPrimeFac 0 = sSup {p | Prime p ∧ p ∣ 0} simpa using (Set.Infinite.Nat.sSup_eq_zero infinite_setOfPred_prime).symmAll goals completed! 🐙
  ·inrn:ℕhn_one:n ≠ 1hn:1 < n⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n} have h_lub : IsLUB {p : ℕ | p.Prime ∧ p ∣ n} (maxPrimeFac n) :=
      isLeast_maxPrimeFac hninrn:ℕhn_one:n ≠ 1hn:1 < nh_lub:IsLUB {p | Prime p ∧ p ∣ n} n.maxPrimeFac⊢ n.maxPrimeFac = sSup {p | Prime p ∧ p ∣ n}
    exact (h_lub.csSup_eq
      ⟨maxPrimeFac n, prime_maxPrimeFac_of_one_lt n hn, maxPrimeFac_dvd⟩).symmAll goals completed! 🐙

@[simp]
lemma one_lt_maxPrimeFac_iff (n : ℕ) :
    1 < maxPrimeFac n ↔ 1 < n := byn:ℕ⊢ 1 < n.maxPrimeFac ↔ 1 < n
  rcases lt_trichotomy n 1 with hn | rfl | hninln:ℕhn:n < 1⊢ 1 < n.maxPrimeFac ↔ 1 < ninr.inl⊢ 1 < maxPrimeFac 1 ↔ 1 < 1inr.inrn:ℕhn:1 < n⊢ 1 < n.maxPrimeFac ↔ 1 < n
  ·inln:ℕhn:n < 1⊢ 1 < n.maxPrimeFac ↔ 1 < n simp only [lt_one_iff] at hninln:ℕhn:n = 0⊢ 1 < n.maxPrimeFac ↔ 1 < n
    simp [hn]All goals completed! 🐙
  ·inr.inl⊢ 1 < maxPrimeFac 1 ↔ 1 < 1 simpAll goals completed! 🐙
  ·inr.inrn:ℕhn:1 < n⊢ 1 < n.maxPrimeFac ↔ 1 < n simpa [hn] using (prime_maxPrimeFac_of_one_lt n hn).one_ltAll goals completed! 🐙

end Nat