Mathlib.Data.Nat.Factors

Nat.primeFactorsList definition

: ℕ → List ℕ

Full source

/-- `primeFactorsList n` is the prime factorization of `n`, listed in increasing order. -/
def primeFactorsList : ℕ → List ℕ
  | 0 => []
  | 1 => []
  | k + 2 =>
    let m := minFac (k + 2)
    m :: primeFactorsList ((k + 2) / m)
decreasing_by exact factors_lemma

List of prime factors of a natural number

Informal description

The function `primeFactorsList` takes a natural number $n$ and returns the list of its prime factors in increasing order. For $n = 0$ or $n = 1$, it returns the empty list. For $n \geq 2$, it recursively constructs the list by appending the smallest prime factor of $n$ to the list of prime factors of $n$ divided by its smallest prime factor.

Nat.primeFactorsList_zero theorem

: primeFactorsList 0 = []

Full source

@[simp]
theorem primeFactorsList_zero : primeFactorsList 0 = [] := by rw [primeFactorsList]

Prime Factors of Zero is Empty List

Informal description

The list of prime factors of the natural number $0$ is the empty list, i.e., $\text{primeFactorsList}(0) = []$.

Nat.primeFactorsList_one theorem

: primeFactorsList 1 = []

Full source

@[simp]
theorem primeFactorsList_one : primeFactorsList 1 = [] := by rw [primeFactorsList]

Prime Factors of One is Empty List

Informal description

The list of prime factors of the natural number $1$ is the empty list, i.e., $\text{primeFactorsList}(1) = []$.

Nat.primeFactorsList_two theorem

: primeFactorsList 2 = [2]

Full source

@[simp]
theorem primeFactorsList_two : primeFactorsList 2 = [2] := by simp [primeFactorsList]

Prime Factorization of Two is $[2]$

Informal description

The list of prime factors of the natural number $2$ is the singleton list $[2]$, i.e., $\text{primeFactorsList}(2) = [2]$.

Nat.prime_of_mem_primeFactorsList theorem

{n : ℕ} : ∀ {p : ℕ}, p ∈ primeFactorsList n → Prime p

Full source

theorem prime_of_mem_primeFactorsList {n : ℕ} : ∀ {p : ℕ}, p ∈ primeFactorsList n → Prime p := by
  match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro p h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
        List.mem_cons.1 (by rwa [primeFactorsList] at h)
      exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList

Elements of Prime Factorization List are Prime

Informal description

For any natural number $n$ and any prime number $p$ in the list of prime factors of $n$, $p$ is indeed a prime number.

Nat.pos_of_mem_primeFactorsList theorem

{n p : ℕ} (h : p ∈ primeFactorsList n) : 0 < p

Full source

theorem pos_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ primeFactorsList n) : 0 < p :=
  Prime.pos (prime_of_mem_primeFactorsList h)

Positivity of Prime Factors in Factorization List

Informal description

For any natural numbers $n$ and $p$, if $p$ is in the list of prime factors of $n$, then $p$ is positive, i.e., $0 < p$.

Nat.prod_primeFactorsList theorem

: ∀ {n}, n ≠ 0 → List.prod (primeFactorsList n) = n

Full source

theorem prod_primeFactorsList : ∀ {n}, n ≠ 0 → List.prod (primeFactorsList n) = n
  | 0 => by simp
  | 1 => by simp
  | k + 2 => fun _ =>
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    show (primeFactorsList (k + 2)).prod = (k + 2) by
      have h₁ : (k + 2) / m ≠ 0 := fun h => by
        have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
        rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
      rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]

Product of Prime Factors Equals Original Number

Informal description

For any nonzero natural number $n$, the product of all prime factors in the list $\text{primeFactorsList}(n)$ equals $n$. That is, if $n \neq 0$, then \[ \prod_{p \in \text{primeFactorsList}(n)} p = n. \]

Nat.primeFactorsList_prime theorem

{p : ℕ} (hp : Nat.Prime p) : p.primeFactorsList = [p]

Full source

theorem primeFactorsList_prime {p : ℕ} (hp : Nat.Prime p) : p.primeFactorsList = [p] := by
  have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl
  rw [this, primeFactorsList]
  simp only [Eq.symm this]
  have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
  simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

Prime Factors List of a Prime Number is the Singleton List

Informal description

For any prime natural number $p$, the list of its prime factors consists of $p$ itself, i.e., $\mathrm{primeFactorsList}(p) = [p]$.

Nat.primeFactorsList_chain theorem

{n : ℕ} : ∀ {a}, (∀ p, Prime p → p ∣ n → a ≤ p) → List.Chain (· ≤ ·) a (primeFactorsList n)

Full source

theorem primeFactorsList_chain {n : ℕ} :
    ∀ {a}, (∀ p, Prime p → p ∣ n → a ≤ p) → List.Chain (· ≤ ·) a (primeFactorsList n) := by
  match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro a h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      rw [primeFactorsList]
      refine List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (primeFactorsList_chain ?_)
      exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Lower Bound Implies Non-Decreasing Prime Factor List

Informal description

For any natural number $n$ and any $a$, if for every prime $p$ dividing $n$ we have $a \leq p$, then the list of prime factors of $n$ (in increasing order) forms a chain where each element is greater than or equal to the previous one, starting from $a$. In other words, if $a$ is a lower bound for all prime divisors of $n$, then $\text{primeFactorsList}(n)$ is a non-decreasing list with all elements $\geq a$.

Nat.primeFactorsList_chain_2 theorem

(n) : List.Chain (· ≤ ·) 2 (primeFactorsList n)

Full source

theorem primeFactorsList_chain_2 (n) : List.Chain (· ≤ ·) 2 (primeFactorsList n) :=
  primeFactorsList_chain fun _ pp _ => pp.two_le

Prime Factors List is Non-Decreasing and Bounded Below by 2

Informal description

For any natural number $n$, the list of its prime factors, $\mathrm{primeFactorsList}(n)$, forms a non-decreasing chain starting from $2$ (i.e., each element is greater than or equal to the previous one, and all elements are $\geq 2$).

Nat.primeFactorsList_chain' theorem

(n) : List.Chain' (· ≤ ·) (primeFactorsList n)

Full source

theorem primeFactorsList_chain' (n) : List.Chain' (· ≤ ·) (primeFactorsList n) :=
  @List.Chain'.tail _ _ (_ :: _) (primeFactorsList_chain_2 _)

Prime Factors List is Non-Decreasing

Informal description

For any natural number $n$, the list of its prime factors, $\mathrm{primeFactorsList}(n)$, is non-decreasing (i.e., each element is less than or equal to the next one).

Nat.primeFactorsList_sorted theorem

(n : ℕ) : List.Sorted (· ≤ ·) (primeFactorsList n)

Full source

theorem primeFactorsList_sorted (n : ℕ) : List.Sorted (· ≤ ·) (primeFactorsList n) :=
  List.chain'_iff_pairwise.1 (primeFactorsList_chain' _)

Prime Factors List is Sorted in Non-Decreasing Order

Informal description

For any natural number $n$, the list of prime factors of $n$ returned by $\mathrm{primeFactorsList}(n)$ is sorted in non-decreasing order.

Nat.primeFactorsList_add_two theorem

(n : ℕ) : primeFactorsList (n + 2) = minFac (n + 2) :: primeFactorsList ((n + 2) / minFac (n + 2))

Full source

/-- `primeFactorsList` can be constructed inductively by extracting `minFac`, for sufficiently
large `n`. -/
theorem primeFactorsList_add_two (n : ℕ) :
    primeFactorsList (n + 2) = minFacminFac (n + 2) :: primeFactorsList ((n + 2) / minFac (n + 2)) := by
  rw [primeFactorsList]

Recursive Construction of Prime Factors List for $n + 2$

Informal description

For any natural number $n$, the list of prime factors of $n + 2$ is obtained by prepending the smallest prime factor of $n + 2$ to the list of prime factors of $(n + 2)$ divided by its smallest prime factor. That is, \[ \text{primeFactorsList}(n + 2) = \text{minFac}(n + 2) :: \text{primeFactorsList}\left(\frac{n + 2}{\text{minFac}(n + 2)}\right). \]

Nat.primeFactorsList_eq_nil theorem

(n : ℕ) : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Full source

@[simp]
theorem primeFactorsList_eq_nil (n : ℕ) : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1 := by
  constructor <;> intro h
  · rcases n with (_ | _ | n)
    · exact Or.inl rfl
    · exact Or.inr rfl
    · rw [primeFactorsList] at h
      injection h
  · rcases h with (rfl | rfl)
    · exact primeFactorsList_zero
    · exact primeFactorsList_one

Empty Prime Factors List Characterization for Natural Numbers

Informal description

For any natural number $n$, the list of prime factors of $n$ is empty if and only if $n = 0$ or $n = 1$.

Nat.mem_primeFactorsList_iff_dvd theorem

{n p : ℕ} (hn : n ≠ 0) (hp : Prime p) : p ∈ primeFactorsList n ↔ p ∣ n

Full source

theorem mem_primeFactorsList_iff_dvd {n p : ℕ} (hn : n ≠ 0) (hp : Prime p) :
    p ∈ primeFactorsList np ∈ primeFactorsList n ↔ p ∣ n where
  mp h := prod_primeFactorsList hn ▸ List.dvd_prod h
  mpr h := mem_list_primes_of_dvd_prod (prime_iff.mp hp)
    (fun _ h ↦ prime_iff.mp (prime_of_mem_primeFactorsList h)) ((prod_primeFactorsList hn).symm ▸ h)

Characterization of Prime Factors via Divisibility

Informal description

For any nonzero natural number $n$ and any prime number $p$, the prime $p$ appears in the list of prime factors of $n$ if and only if $p$ divides $n$. In other words: \[ p \in \text{primeFactorsList}(n) \leftrightarrow p \mid n. \]

Nat.dvd_of_mem_primeFactorsList theorem

{n p : ℕ} (h : p ∈ n.primeFactorsList) : p ∣ n

Full source

theorem dvd_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ∣ n := by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · exact dvd_zero p
  · rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

Divisibility by Prime Factors in Natural Numbers

Informal description

For any natural numbers $n$ and $p$, if $p$ is in the list of prime factors of $n$, then $p$ divides $n$.

Nat.mem_primeFactorsList theorem

{n p} (hn : n ≠ 0) : p ∈ primeFactorsList n ↔ Prime p ∧ p ∣ n

Full source

theorem mem_primeFactorsList {n p} (hn : n ≠ 0) : p ∈ primeFactorsList np ∈ primeFactorsList n ↔ Prime p ∧ p ∣ n :=
  ⟨fun h => ⟨prime_of_mem_primeFactorsList h, dvd_of_mem_primeFactorsList h⟩, fun ⟨hprime, hdvd⟩ =>
    (mem_primeFactorsList_iff_dvd hn hprime).mpr hdvd⟩

Characterization of Prime Factors in Factorization List

Informal description

For any nonzero natural number $n$ and any natural number $p$, the prime $p$ belongs to the list of prime factors of $n$ if and only if $p$ is prime and $p$ divides $n$. In symbols: \[ p \in \text{primeFactorsList}(n) \leftrightarrow \text{Prime}(p) \land p \mid n. \]

Nat.mem_primeFactorsList' theorem

{n p} : p ∈ n.primeFactorsList ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0

Full source

@[simp] lemma mem_primeFactorsList' {n p} : p ∈ n.primeFactorsListp ∈ n.primeFactorsList ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
  cases n <;> simp [mem_primeFactorsList, *]

Characterization of Prime Factors in a Natural Number's Factorization List

Informal description

For any natural numbers $n$ and $p$, the prime $p$ belongs to the list of prime factors of $n$ if and only if $p$ is prime, $p$ divides $n$, and $n \neq 0$. In symbols: $$p \in \text{primeFactorsList}(n) \leftrightarrow \text{Prime}(p) \land p \mid n \land n \neq 0.$$

Nat.le_of_mem_primeFactorsList theorem

{n p : ℕ} (h : p ∈ n.primeFactorsList) : p ≤ n

Full source

theorem le_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ≤ n := by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · rw [primeFactorsList_zero] at h
    cases h
  · exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

Prime Factors Are Bounded by Their Number

Informal description

For any natural numbers $n$ and $p$, if $p$ is in the list of prime factors of $n$, then $p \leq n$.

Nat.primeFactorsList_unique theorem

{n : ℕ} {l : List ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, Prime p) : l ~ primeFactorsList n

Full source

/-- **Fundamental theorem of arithmetic** -/
theorem primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, Prime p) :
    l ~ primeFactorsList n := by
  refine perm_of_prod_eq_prod ?_ ?_ ?_
  · rw [h₁]
    refine (prod_primeFactorsList ?_).symm
    rintro rfl
    rw [prod_eq_zero_iff] at h₁
    exact Prime.ne_zero (h₂ 0 h₁) rfl
  · simp_rw [← prime_iff]
    exact h₂
  · simp_rw [← prime_iff]
    exact fun p => prime_of_mem_primeFactorsList

Uniqueness of Prime Factorization up to Permutation

Informal description

For any natural number $n$ and any list of natural numbers $l$, if the product of the elements in $l$ equals $n$ and every element in $l$ is prime, then $l$ is a permutation of the list of prime factors of $n$ (i.e., $l \sim \text{primeFactorsList}(n)$).

Nat.Prime.primeFactorsList_pow theorem

{p : ℕ} (hp : p.Prime) (n : ℕ) : (p ^ n).primeFactorsList = List.replicate n p

Full source

theorem Prime.primeFactorsList_pow {p : ℕ} (hp : p.Prime) (n : ℕ) :
    (p ^ n).primeFactorsList = List.replicate n p := by
  symm
  rw [← List.replicate_perm]
  apply Nat.primeFactorsList_unique (List.prod_replicate n p)
  intro q hq
  rwa [eq_of_mem_replicate hq]

Prime Factorization of Power of a Prime: $\text{primeFactorsList}(p^n) = [p, \ldots, p]$ ($n$ times)

Informal description

For any prime natural number $p$ and any natural number $n$, the list of prime factors of $p^n$ is the list consisting of $n$ copies of $p$, i.e., $\text{primeFactorsList}(p^n) = [p, \ldots, p]$ (with $p$ repeated $n$ times).

Nat.perm_primeFactorsList_mul theorem

{a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Full source

/-- For positive `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
theorem perm_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList := by
  refine (primeFactorsList_unique ?_ ?_).symm
  · rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
  · intro p hp
    rw [List.mem_append] at hp
    rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'

Prime Factorization of Product is Union of Factors

Informal description

For any nonzero natural numbers $a$ and $b$, the list of prime factors of $a \cdot b$ is a permutation of the concatenation of the prime factors of $a$ and the prime factors of $b$. That is, \[ \text{primeFactorsList}(a \cdot b) \sim \text{primeFactorsList}(a) +\!\!\!+ \text{primeFactorsList}(b). \]

Nat.perm_primeFactorsList_mul_of_coprime theorem

{a b : ℕ} (hab : Coprime a b) : (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Full source

/-- For coprime `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
theorem perm_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList := by
  rcases a.eq_zero_or_pos with (rfl | ha)
  · simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  · simp [(coprime_zero_right _).mp hab]
  exact perm_primeFactorsList_mul ha.ne' hb.ne'

Prime Factorization of Coprime Product is Union of Factors

Informal description

For any coprime natural numbers $a$ and $b$, the list of prime factors of $a \cdot b$ is a permutation of the concatenation of the prime factors of $a$ and the prime factors of $b$. That is, \[ \text{primeFactorsList}(a \cdot b) \sim \text{primeFactorsList}(a) +\!\!\!+ \text{primeFactorsList}(b). \]

Nat.primeFactorsList_sublist_right theorem

{n k : ℕ} (h : k ≠ 0) : n.primeFactorsList <+ (n * k).primeFactorsList

Full source

theorem primeFactorsList_sublist_right {n k : ℕ} (h : k ≠ 0) :
    n.primeFactorsList <+ (n * k).primeFactorsList := by
  rcases n with - | hn
  · simp [zero_mul]
  apply sublist_of_subperm_of_sorted _ (primeFactorsList_sorted _) (primeFactorsList_sorted _)
  simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]
  exact (sublist_append_left _ _).subperm

Prime Factors Sublist Property for Multiplication by Nonzero Natural Number

Informal description

For any natural numbers $n$ and $k$ with $k \neq 0$, the list of prime factors of $n$ is a sublist of the list of prime factors of $n \cdot k$.

Nat.primeFactorsList_sublist_of_dvd theorem

{n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList <+ k.primeFactorsList

Full source

theorem primeFactorsList_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
    n.primeFactorsList <+ k.primeFactorsList := by
  obtain ⟨a, rfl⟩ := h
  exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Sublist Property of Prime Factors under Divisibility

Informal description

For any natural numbers $n$ and $k$ such that $n$ divides $k$ and $k \neq 0$, the list of prime factors of $n$ is a sublist of the list of prime factors of $k$.

Nat.primeFactorsList_subset_right theorem

{n k : ℕ} (h : k ≠ 0) : n.primeFactorsList ⊆ (n * k).primeFactorsList

Full source

theorem primeFactorsList_subset_right {n k : ℕ} (h : k ≠ 0) :
    n.primeFactorsList ⊆ (n * k).primeFactorsList :=
  (primeFactorsList_sublist_right h).subset

Prime Factors Subset Property for Multiplication by Nonzero Natural Number

Informal description

For any natural numbers $n$ and $k$ with $k \neq 0$, the set of prime factors of $n$ is a subset of the set of prime factors of $n \cdot k$.

Nat.primeFactorsList_subset_of_dvd theorem

{n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList ⊆ k.primeFactorsList

Full source

theorem primeFactorsList_subset_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
    n.primeFactorsList ⊆ k.primeFactorsList :=
  (primeFactorsList_sublist_of_dvd h h').subset

Prime Factor Subset Property under Divisibility

Informal description

For any natural numbers $n$ and $k$ such that $n$ divides $k$ and $k \neq 0$, the set of prime factors of $n$ is a subset of the set of prime factors of $k$.

Nat.dvd_of_primeFactorsList_subperm theorem

{a b : ℕ} (ha : a ≠ 0) (h : a.primeFactorsList <+~ b.primeFactorsList) : a ∣ b

Full source

theorem dvd_of_primeFactorsList_subperm {a b : ℕ} (ha : a ≠ 0)
    (h : a.primeFactorsList <+~ b.primeFactorsList) : a ∣ b := by
  rcases b.eq_zero_or_pos with (rfl | hb)
  · exact dvd_zero _
  rcases a with (_ | _ | a)
  · exact (ha rfl).elim
  · exact one_dvd _
  use (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
  nth_rw 1 [← Nat.prod_primeFactorsList ha]
  rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']

Divisibility via Subpermutation of Prime Factor Lists

Informal description

For any nonzero natural numbers $a$ and $b$, if the list of prime factors of $a$ is a subpermutation of the list of prime factors of $b$, then $a$ divides $b$.

Nat.replicate_subperm_primeFactorsList_iff theorem

{a b n : ℕ} (ha : Prime a) (hb : b ≠ 0) : replicate n a <+~ primeFactorsList b ↔ a ^ n ∣ b

Full source

theorem replicate_subperm_primeFactorsList_iff {a b n : ℕ} (ha : Prime a) (hb : b ≠ 0) :
    replicatereplicate n a <+~ primeFactorsList breplicate n a <+~ primeFactorsList b ↔ a ^ n ∣ b := by
  induction n generalizing b with
  | zero => simp
  | succ n ih =>
    constructor
    · rw [List.subperm_iff]
      rintro ⟨u, hu1, hu2⟩
      rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
      exact hu2.prod_dvd_prod
    · rintro ⟨c, rfl⟩
      rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
      rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]
      exact dvd_mul_right _ _

Subpermutation of Prime Factors Characterizes Divisibility by Power of Prime

Informal description

For any prime natural number $a$, any nonzero natural number $b$, and any natural number $n$, the list consisting of $n$ copies of $a$ is a subpermutation of the list of prime factors of $b$ if and only if $a^n$ divides $b$. In other words, \[ \text{replicate}(n, a) \prec\!\!\sim \text{primeFactorsList}(b) \leftrightarrow a^n \mid b. \]

Nat.mem_primeFactorsList_mul theorem

 {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
  p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Full source

theorem mem_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
    p ∈ (a * b).primeFactorsListp ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList := by
  rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
    ← and_or_left]
  simpa only [and_congr_right_iff] using Prime.dvd_mul

Prime Factorization of Product: $p \in \text{primeFactorsList}(a \cdot b) \leftrightarrow p \in \text{primeFactorsList}(a) \lor p \in \text{primeFactorsList}(b)$

Informal description

For any nonzero natural numbers $a$ and $b$, and any natural number $p$, the prime $p$ belongs to the list of prime factors of the product $a \cdot b$ if and only if $p$ belongs to the list of prime factors of $a$ or to the list of prime factors of $b$. In symbols: \[ p \in \text{primeFactorsList}(a \cdot b) \leftrightarrow p \in \text{primeFactorsList}(a) \lor p \in \text{primeFactorsList}(b). \]

Nat.coprime_primeFactorsList_disjoint theorem

{a b : ℕ} (hab : a.Coprime b) : List.Disjoint a.primeFactorsList b.primeFactorsList

Full source

/-- The sets of factors of coprime `a` and `b` are disjoint -/
theorem coprime_primeFactorsList_disjoint {a b : ℕ} (hab : a.Coprime b) :
    List.Disjoint a.primeFactorsList b.primeFactorsList := by
  intro q hqa hqb
  apply not_prime_one
  rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
    (dvd_of_mem_primeFactorsList hqb)]
  exact prime_of_mem_primeFactorsList hqa

Disjointness of Prime Factor Lists for Coprime Numbers

Informal description

For any two coprime natural numbers $a$ and $b$, the lists of their prime factors are disjoint. That is, if $a$ and $b$ are coprime, then no prime number appears in both $\text{primeFactorsList}(a)$ and $\text{primeFactorsList}(b)$.

Nat.mem_primeFactorsList_mul_of_coprime theorem

 {a b : ℕ} (hab : Coprime a b) (p : ℕ) : p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Full source

theorem mem_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) (p : ℕ) :
    p ∈ (a * b).primeFactorsListp ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList := by
  rcases a.eq_zero_or_pos with (rfl | ha)
  · simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  · simp [(coprime_zero_right _).mp hab]
  rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

Prime Factorization of Coprime Product: $p \in \text{primeFactorsList}(a \cdot b) \leftrightarrow p \in \text{primeFactorsList}(a) \cup \text{primeFactorsList}(b)$ for coprime $a, b$

Informal description

For any two coprime natural numbers $a$ and $b$, and any natural number $p$, the prime $p$ belongs to the list of prime factors of the product $a \cdot b$ if and only if $p$ belongs to the union of the lists of prime factors of $a$ and $b$. In symbols: \[ p \in \text{primeFactorsList}(a \cdot b) \leftrightarrow p \in \text{primeFactorsList}(a) \cup \text{primeFactorsList}(b). \]

Nat.mem_primeFactorsList_mul_left theorem

{p a b : ℕ} (hpa : p ∈ a.primeFactorsList) (hb : b ≠ 0) : p ∈ (a * b).primeFactorsList

Full source

/-- If `p` is a prime factor of `a` then `p` is also a prime factor of `a * b` for any `b > 0` -/
theorem mem_primeFactorsList_mul_left {p a b : ℕ} (hpa : p ∈ a.primeFactorsList) (hb : b ≠ 0) :
    p ∈ (a * b).primeFactorsList := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp at hpa
  apply (mem_primeFactorsList_mul ha hb).2 (Or.inl hpa)

Prime Factor Inheritance in Products: Left Multiplicand Case

Informal description

For any natural numbers $p$, $a$, and $b$ with $b \neq 0$, if $p$ is a prime factor of $a$ (i.e., $p \in \text{primeFactorsList}(a)$), then $p$ is also a prime factor of the product $a \cdot b$ (i.e., $p \in \text{primeFactorsList}(a \cdot b)$).

Nat.mem_primeFactorsList_mul_right theorem

{p a b : ℕ} (hpb : p ∈ b.primeFactorsList) (ha : a ≠ 0) : p ∈ (a * b).primeFactorsList

Full source

/-- If `p` is a prime factor of `b` then `p` is also a prime factor of `a * b` for any `a > 0` -/
theorem mem_primeFactorsList_mul_right {p a b : ℕ} (hpb : p ∈ b.primeFactorsList) (ha : a ≠ 0) :
    p ∈ (a * b).primeFactorsList := by
  rw [mul_comm]
  exact mem_primeFactorsList_mul_left hpb ha

Prime Factor Inheritance in Products: Right Multiplicand Case

Informal description

For any natural numbers $p$, $a$, and $b$ with $a \neq 0$, if $p$ is a prime factor of $b$ (i.e., $p \in \text{primeFactorsList}(b)$), then $p$ is also a prime factor of the product $a \cdot b$ (i.e., $p \in \text{primeFactorsList}(a \cdot b)$).

Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt theorem

{n : ℕ} (n2 : 2 < n) : 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Full source

theorem four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : ℕ} (n2 : 2 < n) :
    4 ∣ n4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p := by
  obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
  · contradiction
  · contradiction
  · simp [Nat.pow_succ, mul_assoc]
  · exact Or.inr ⟨p, hp, hdvd, hodd⟩

Every natural number greater than 2 is either divisible by 4 or has an odd prime factor

Informal description

For any natural number $n > 2$, either $4$ divides $n$, or there exists an odd prime number $p$ that divides $n$.

Important declarations