A272032 proof

import Mathlib

/-!
A272032: arithmetic core of the implication

  exact quotient prime  ->  exponent prime.

The quotient is represented by an explicit natural number `T` together with

  (q + r) * T = q ^ n + r ^ n.

This is intentional: `Nat.div` is truncated division and would not express the
OEIS condition that the rational quotient is an integer.
-/

namespace A272032

/-- The exact natural-number quotient occurring in A272032. -/
def ExactQuotient (n q r T : ℕ) : Prop :=
  (q + r) * T = q ^ n + r ^ n

private theorem odd_composite_case
    {n q r T : ℕ}
    (hn : 3 ≤ n)
    (hnOdd : Odd n)
    (hnComp : ¬ Nat.Prime n)
    (hqr : 0 < q + r)
    (hqOdd : Odd q)
    (hrOdd : Odd r)
    (hquot : ExactQuotient n q r T)
    (hT : Nat.Prime T) : False := by
  rcases (Nat.not_prime_iff_exists_mul_eq (by omega : 2 ≤ n)).mp hnComp with
    ⟨a, b, ha_lt, hb_lt, hab⟩

  have ha0 : a ≠ 0 := by
    intro ha
    subst a
    simp at hab
    omega
  have ha1 : a ≠ 1 := by
    intro ha
    subst a
    simp at hab
    omega
  have hb0 : b ≠ 0 := by
    intro hb
    subst b
    simp at hab
    omega
  have hb1 : b ≠ 1 := by
    intro hb
    subst b
    simp at hab
    omega
  have ha2 : 2 ≤ a := by omega
  have hb2 : 2 ≤ b := by omega

  have habOdd : Odd (a * b) := hab.symm ▸ hnOdd
  have haOdd : Odd a := Nat.Odd.of_mul_left habOdd
  have hbOdd : Odd b := Nat.Odd.of_mul_right habOdd

  have hdivA : q + r ∣ q ^ a + r ^ a :=
    haOdd.nat_add_dvd_pow_add_pow q r
  rcases hdivA with ⟨A, hA⟩

  have hdivB : q ^ a + r ^ a ∣ (q ^ a) ^ b + (r ^ a) ^ b :=
    hbOdd.nat_add_dvd_pow_add_pow (q ^ a) (r ^ a)
  rcases hdivB with ⟨B, hB⟩

  have hnum : q ^ n + r ^ n = (q ^ a + r ^ a) * B := by
    calc
      q ^ n + r ^ n = q ^ (a * b) + r ^ (a * b) := by rw [hab]
      _ = (q ^ a) ^ b + (r ^ a) ^ b := by simp [pow_mul]
      _ = (q ^ a + r ^ a) * B := hB

  have hfac0 : (q + r) * (A * B) = (q + r) * T := by
    calc
      (q + r) * (A * B) = ((q + r) * A) * B := by simp [mul_assoc]
      _ = (q ^ a + r ^ a) * B := by rw [← hA]
      _ = q ^ n + r ^ n := hnum.symm
      _ = (q + r) * T := hquot.symm
  have hfac : A * B = T := Nat.mul_left_cancel hqr hfac0

  by_cases hones : q = 1 ∧ r = 1
  · rcases hones with ⟨rfl, rfl⟩
    simp [ExactQuotient] at hquot
    have hT1 : T = 1 := by omega
    exact hT.ne_one hT1

  have hq1 : 1 ≤ q := by
    rcases hqOdd with ⟨k, hk⟩
    omega
  have hr1 : 1 ≤ r := by
    rcases hrOdd with ⟨k, hk⟩
    omega
  have hbig : 1 < q ∨ 1 < r := by
    by_contra h
    push Not at h
    apply hones
    constructor <;> omega

  have hsumA : q + r < q ^ a + r ^ a := by
    rcases hbig with hq | hr
    · have hqa : q < q ^ a := by
        simpa using (Nat.pow_lt_pow_right hq (show 1 < a by omega))
      have hra : r ≤ r ^ a := le_self_pow hr1 ha0
      omega
    · have hqa : q ≤ q ^ a := le_self_pow hq1 ha0
      have hra : r < r ^ a := by
        simpa using (Nat.pow_lt_pow_right hr (show 1 < a by omega))
      omega

  have hsumB : q ^ a + r ^ a < q ^ n + r ^ n := by
    rcases hbig with hq | hr
    · have hqpow : q ^ a < q ^ n :=
        Nat.pow_lt_pow_right hq ha_lt
      have hrpow : r ^ a ≤ r ^ n :=
        pow_le_pow_right' hr1 (Nat.le_of_lt ha_lt)
      omega
    · have hqpow : q ^ a ≤ q ^ n :=
        pow_le_pow_right' hq1 (Nat.le_of_lt ha_lt)
      have hrpow : r ^ a < r ^ n :=
        Nat.pow_lt_pow_right hr ha_lt
      omega

  have hAne : A ≠ 1 := by
    intro hA1
    subst A
    simp at hA
    omega
  have hBne : B ≠ 1 := by
    intro hB1
    subst B
    simp at hnum
    omega

  exact (Nat.not_prime_of_mul_eq hfac hAne hBne) hT

private theorem even_case
    {n q r T : ℕ}
    (hn : 3 ≤ n)
    (hnEven : Even n)
    (hqr : 0 < q + r)
    (hqEven : Even q)
    (hrEven : Even r)
    (hgap : q + r < 2 ^ (n - 1))
    (hquot : ExactQuotient n q r T)
    (hT : Nat.Prime T) : False := by
  have hn0 : n ≠ 0 := by omega

  have h2q : 2 ^ n ∣ q ^ n :=
    pow_dvd_pow_of_dvd hqEven.two_dvd n
  have h2r : 2 ^ n ∣ r ^ n :=
    pow_dvd_pow_of_dvd hrEven.two_dvd n
  have h2sum : 2 ^ n ∣ q ^ n + r ^ n := h2q.add h2r
  have h2prod : 2 ^ n ∣ (q + r) * T := by
    rw [hquot]
    exact h2sum

  have hnotOdd : ¬ Odd T := by
    intro hTodd
    have hcop : Nat.Coprime (2 ^ n) T :=
      (hTodd.coprime_two_left).pow_left n
    have h2den : 2 ^ n ∣ q + r :=
      hcop.dvd_of_dvd_mul_right h2prod
    have hpow_le : 2 ^ n ≤ q + r := Nat.le_of_dvd hqr h2den
    have hpow_lt : 2 ^ (n - 1) < 2 ^ n :=
      Nat.pow_lt_pow_right (by norm_num : 1 < (2 : ℕ)) (Nat.sub_one_lt hn0)
    omega

  rcases hT.eq_two_or_odd' with hT2 | hTodd
  · have hqr2 : 2 ≤ q ∨ 2 ≤ r := by
      rcases (even_iff_exists_two_mul.mp hqEven) with ⟨q₀, hq⟩
      rcases (even_iff_exists_two_mul.mp hrEven) with ⟨r₀, hr⟩
      omega

    have hlower : 2 ^ n ≤ q ^ n + r ^ n := by
      rcases hqr2 with hq2 | hr2
      · have hp : 2 ^ n ≤ q ^ n := Nat.pow_le_pow_left hq2 n
        omega
      · have hp : 2 ^ n ≤ r ^ n := Nat.pow_le_pow_left hr2 n
        omega

    have hnumEq : q ^ n + r ^ n = 2 * (q + r) := by
      calc
        q ^ n + r ^ n = (q + r) * T := hquot.symm
        _ = (q + r) * 2 := by rw [hT2]
        _ = 2 * (q + r) := by omega

    have hmulLt : 2 * (q + r) < 2 * 2 ^ (n - 1) :=
      Nat.mul_lt_mul_of_pos_left hgap (by norm_num)

    have hpowEq : 2 * 2 ^ (n - 1) = 2 ^ n := by
      cases n with
      | zero => omega
      | succ k => simp [pow_succ, Nat.mul_comm]

    have hupper : q ^ n + r ^ n < 2 ^ n := by
      calc
        q ^ n + r ^ n = 2 * (q + r) := hnumEq
        _ < 2 * 2 ^ (n - 1) := hmulLt
        _ = 2 ^ n := hpowEq
    omega
  · exact hnotOdd hTodd

/--
Arithmetic core of the A272032 argument.

The three hypotheses `hodd_qr`, `heven_qr`, and `hgap` are exactly the local
facts supplied by the immediately preceding/following primes:

* odd `n` gives odd `q,r`;
* even `n` gives even `q,r`;
* Bertrand's postulate gives `q+r < 2^(n-1)` for the relevant even case.
-/
theorem prime_exponent_of_prime_exactQuotient
    {n q r T : ℕ}
    (hn : 3 ≤ n)
    (hqr : 0 < q + r)
    (hodd_qr : Odd n → Odd q ∧ Odd r)
    (heven_qr : Even n → Even q ∧ Even r)
    (hgap : q + r < 2 ^ (n - 1))
    (hquot : ExactQuotient n q r T)
    (hT : Nat.Prime T) : Nat.Prime n := by
  by_contra hnComp
  rcases Nat.even_or_odd n with hnEven | hnOdd
  · rcases heven_qr hnEven with ⟨hqEven, hrEven⟩
    exact even_case hn hnEven hqr hqEven hrEven hgap hquot hT
  · rcases hodd_qr hnOdd with ⟨hqOdd, hrOdd⟩
    exact odd_composite_case hn hnOdd hnComp hqr hqOdd hrOdd hquot hT


/-! ## End-to-end OEIS formulation -/

/-- `p` is the prime immediately preceding `n`. -/
def IsPreviousPrime (p n : ℕ) : Prop :=
  Nat.Prime p ∧ p < n ∧
    ∀ ℓ : ℕ, Nat.Prime ℓ → ℓ < n → ℓ ≤ p

/-- `p` is the prime immediately following `n`. -/
def IsNextPrime (p n : ℕ) : Prop :=
  Nat.Prime p ∧ n < p ∧
    ∀ ℓ : ℕ, Nat.Prime ℓ → n < ℓ → p ≤ ℓ

/--
Full A272032 theorem with explicit neighboring primes and explicit values of
`q` and `r`.

The hypotheses `hq` and `hr` say exactly that `q` and `r` count the composite
integers between `n` and its neighboring primes.  `hquot` says the quotient is
an exact natural number, not a truncated `Nat.div`.
-/
theorem oeis_A272032_of_neighbors
    {n pminus pplus q r T : ℕ}
    (hn : 3 ≤ n)
    (hprev : IsPreviousPrime pminus n)
    (hnext : IsNextPrime pplus n)
    (hq : q = n - pminus - 1)
    (hr : r = pplus - n - 1)
    (hqr : 0 < q + r)
    (hquot : ExactQuotient n q r T)
    (hT : Nat.Prime T) :
    Nat.Prime n := by
  by_contra hnComp

  rcases hprev with ⟨hpminusPrime, hpminus_lt, hpminus_max⟩
  rcases hnext with ⟨hpplusPrime, hn_lt_pplus, hpplus_min⟩

  have hn_ne_three : n ≠ 3 := by
    intro hn3
    subst n
    exact hnComp Nat.prime_three
  have hn4 : 4 ≤ n := by omega

  have hpminus_ne_two : pminus ≠ 2 := by
    intro hp2
    have hthree_le : 3 ≤ pminus :=
      hpminus_max 3 Nat.prime_three (by omega)
    omega
  have hpplus_ne_two : pplus ≠ 2 := by omega

  have hpminusOdd : Odd pminus :=
    hpminusPrime.odd_of_ne_two hpminus_ne_two
  have hpplusOdd : Odd pplus :=
    hpplusPrime.odd_of_ne_two hpplus_ne_two

  have hq_identity : pminus + q + 1 = n := by
    rw [hq]
    omega
  have hr_identity : n + r + 1 = pplus := by
    rw [hr]
    omega

  /- Bertrand gives a prime `p` with `n < p ≤ 2n`; minimality of `pplus`
     then gives `pplus ≤ 2n`. -/
  rcases Nat.bertrand n (by omega : n ≠ 0) with
    ⟨p, hpPrime, hn_lt_p, hp_le_two_n⟩
  have hpplus_le_two_n : pplus ≤ 2 * n :=
    le_trans (hpplus_min p hpPrime hn_lt_p) hp_le_two_n

  /- From the two gap identities, `pminus ≥ 2`, and `pplus ≤ 2n`, we get
     `q+r < 2(n-1)`.  Mathlib's `Nat.mul_le_pow` then supplies
     `2(n-1) ≤ 2^(n-1)`. -/
  have hsmall : q + r < 2 * (n - 1) := by
    have hpminus_two : 2 ≤ pminus := hpminusPrime.two_le
    omega
  have hmul_pow : 2 * (n - 1) ≤ 2 ^ (n - 1) :=
    Nat.mul_le_pow (a := 2) (by norm_num) (n - 1)
  have hgap : q + r < 2 ^ (n - 1) :=
    lt_of_lt_of_le hsmall hmul_pow

  rcases Nat.even_or_odd n with hnEven | hnOdd
  · have hqEven : Even q := by
      have hdiffOdd : Odd (n - pminus) :=
        Nat.Even.sub_odd (Nat.le_of_lt hpminus_lt) hnEven hpminusOdd
      rw [hq]
      exact Nat.Odd.sub_odd hdiffOdd odd_one

    have hrEven : Even r := by
      have hdiffOdd : Odd (pplus - n) :=
        Nat.Odd.sub_even (Nat.le_of_lt hn_lt_pplus) hpplusOdd hnEven
      rw [hr]
      exact Nat.Odd.sub_odd hdiffOdd odd_one

    exact even_case hn hnEven hqr hqEven hrEven hgap hquot hT

  · have hqOdd : Odd q := by
      have hdiffEven : Even (n - pminus) :=
        Nat.Odd.sub_odd hnOdd hpminusOdd
      have hdiff_pos : 1 ≤ n - pminus := by omega
      rw [hq]
      exact Nat.Even.sub_odd hdiff_pos hdiffEven odd_one

    have hrOdd : Odd r := by
      have hdiffEven : Even (pplus - n) :=
        Nat.Odd.sub_odd hpplusOdd hnOdd
      have hdiff_pos : 1 ≤ pplus - n := by omega
      rw [hr]
      exact Nat.Even.sub_odd hdiff_pos hdiffEven odd_one

    exact odd_composite_case hn hnOdd hnComp hqr hqOdd hrOdd hquot hT

/--
The direct form of the theorem, with

`q = n - pminus - 1` and `r = pplus - n - 1`

substituted into the statement.
-/
theorem oeis_A272032
    {n pminus pplus T : ℕ}
    (hn : 3 ≤ n)
    (hprev : IsPreviousPrime pminus n)
    (hnext : IsNextPrime pplus n)
    (hqr : 0 < (n - pminus - 1) + (pplus - n - 1))
    (hquot : ExactQuotient n
      (n - pminus - 1) (pplus - n - 1) T)
    (hT : Nat.Prime T) :
    Nat.Prime n := by
  exact oeis_A272032_of_neighbors
    hn hprev hnext rfl rfl hqr hquot hT

/-- Membership predicate corresponding to the mathematical definition of
A272032 used in this file. -/
def IsA272032Term (n : ℕ) : Prop :=
  ∃ pminus pplus T : ℕ,
    3 ≤ n ∧
    IsPreviousPrime pminus n ∧
    IsNextPrime pplus n ∧
    0 < (n - pminus - 1) + (pplus - n - 1) ∧
    ExactQuotient n (n - pminus - 1) (pplus - n - 1) T ∧
    Nat.Prime T

/-- Every term satisfying the A272032 definition is prime. -/
theorem all_A272032_terms_are_prime {n : ℕ}
    (hn : IsA272032Term n) : Nat.Prime n := by
  rcases hn with
    ⟨pminus, pplus, T, hn3, hprev, hnext, hqr, hquot, hT⟩
  exact oeis_A272032 hn3 hprev hnext hqr hquot hT

#print axioms all_A272032_terms_are_prime

end A272032