Euler function

Stream: mathlib4

[BANGJI HU]

微信图片_20241031233718.jpg
Here is my mathematical proof but I'm not familiar with lean yet

[BANGJI HU]

import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Tactic
import Mathlib
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.Data.Nat.Defs
import Mathlib.Data.Nat.Prime

open Nat

open Nat
open Classical
theorem problem_statement (n : ℕ) (hn : 0 < n) : 2^(n * (n + 1)) ∣ 32 * totient (2^(2^n) - 1) := by
  induction n with
  | zero =>
    exfalso
    exact Nat.not_lt_zero _ hn
  | succ d hd =>
    match d with
    | zero =>
      simp only [zero_eq, zero_add, one_mul, pow_one]
      exact dvd_of_mod_eq_zero rfl
    | succ k =>
      have hd' : 0 < d.succ := by
        simp only [gt_iff_lt, Nat.zero_lt_succ]
      have IH : 2^(d*(d+1)) ∣ 32 * totient (2^(2^d) - 1) :=by sorry
      have hfact : 2^(2^d.succ) - 1 = (2^(2^d) - 1) * (2^(2^d) + 1) := by
        sorry
      have hcoprime : Nat.Coprime (2^(2^d) - 1) (2^(2^d) + 1) := by
        sorry
      have h1 : 2^(d.succ * (d.succ + 1)) ∣ 32 * totient (2^(2^d.succ) - 1) := by
        rw [hfact, Nat.totient_mul hcoprime]
        rw [mul_assoc]
        apply dvd_mul_of_dvd_left
        . suffices h : 2^(d*(d+1)) ∣ 32 * totient (2^(2^d) - 1)
          . apply dvd_mul_of_dvd_left
            rw [←pow_mul, mul_comm]
            exact h.pow (by norm_num)
          exact IH
        suffices h : 2^(2*d.succ) ∣ totient (2^(2^d) + 1)
        . exact h
        by_cases hp : (Prime (2^(2^d) + 1)) ∨ ∃ (p q : ℕ), Prime p ∧ Prime q ∧ p ≠ q ∧ p ∣ 2^(2^d) + 1 ∧ q ∣ 2^(2^d) + 1
        . cases hp with
          | inl hprime =>
            rw [totient_prime]
            . contrapose! hprime with hnprime
              rw [←Nat.prime_def] at hnprime
              apply hnprime
              use 2^(2^d) + 1, 1
              simp
            . suffices : 2^d.succ ≤ ((2^(2^d) + 1) - 2)
              . apply Nat.le_of_dvd
                . norm_num
                . exact Nat.pow_dvd_pow _ this
              calc
                   2^(2^d.succ)
                 = 2^(2*2^d) := by rw [pow_mul]
                <= 2^(2^d + 2^d) := by apply Nat.pow_le_pow_add; simp
                 = 2^(2^d.succ) - 2^(2^d) := by
                   rw [←pow_add, ←pow_one, ←mul_sub, sq]
                <= 2^(2^d) + 1 - 2 := by
                   apply Nat.sub_le_sub_right
                   simp
          | inr ⟨p, q, hp, hq, hne, hdvd1, hdvd2⟩ =>
            have h : 2*d.succ ≤ min (totient p) (totient q) := by
              constructor
              . rw [totient_prime hp]
                by_contra hcontra
                have h' : d.succ ∣ (p - 1) := by
                  rw [←Nat.le_iff_dvd]
                  intro hcontra'
                  have : d.succ < (p - 1) := lt_of_not_ge hcontra'
                  rw [←Nat.dvd_iff_mod_eq_zero, ←Nat.le_iff_dvd] at this
                  apply this.not_le
                  calc
                       2^(2^d.succ)
                     = 2^(2*2^d) := by rw [pow_mul]
                    <= 2^(2^d + 2^d) := by apply Nat.pow_le_pow_add; simp
                     = 2^(2^d.succ) - 2^(2^d) := by
                       rw [←pow_add, ←pow_one, ←mul_sub, sq]
                    <= p - 1 := by
                       apply Nat.sub_le_sub_right
                       apply dvd_le_of_mul_left_dvd (Nat.succ_pos _) hdvd1
                     < p := Nat.sub_lt (Nat.lt_add_one _) zero_lt_one
                have hdvd : 2^d.succ ∣ (p - 1) := by
                  apply Nat.dvd_of_dvd_of_dvd _ (Nat.sub_pos_of_lt (Nat.prime.one_lt hp))
                  apply Nat.dvd_of_dvd_sub
                  . exact dvd_rfl
                  . exact hdvd1
                obtain ⟨k, hk⟩ := Nat.pow_eq_iff_le_iff.mp h'
                apply hcontra
                rw [hk, Nat.pow_dvd_iff_le_right zero_lt_two]
              . rw [totient_prime hq]
                by_contra hcontra
                have h' : d.succ ∣ (q - 1) := by
                  rw [←Nat.le_iff_dvd]
                  intro hcontra'
                  have : d.succ < (q - 1) := lt_of_not_ge hcontra'
                  rw [←Nat.dvd_iff_mod_eq_zero, ←Nat.le_iff_dvd] at this
                  apply this.not_le
                  calc
                       2^(2^d.succ)
                     = 2^(2*2^d) := by rw [pow_mul]
                    <= 2^(2^d + 2^d) := by apply Nat.pow_le_pow_add; simp
                     = 2^(2^d.succ) - 2^(2^d) := by
                       rw [←pow_add, ←pow_one, ←mul_sub, sq]
                    <= q - 1 := by
                       apply Nat.sub_le_sub_right
                       apply dvd_le_of_mul_left_dvd (Nat.succ_pos _) hdvd2
                     < q := Nat.sub_lt (Nat.lt_add_one _) zero_lt_one
                have hdvd : 2^d.succ ∣ (q - 1) := by
                  apply Nat.dvd_of_dvd_of_dvd _ (Nat.sub_pos_of_lt (Nat.prime.one_lt hq))
                  apply Nat.dvd_of_dvd_sub
                  . exact dvd_rfl
                  . exact hdvd2
                obtain ⟨k, hk⟩ := Nat.pow_eq_iff_le_iff.mp h'
                apply hcontra
                rw [hk, Nat.pow_dvd_iff_le_right zero_lt_two]
            have := Nat.pow_dvd_pow_of_dvd_left (2^d.succ) (2*d.succ) (h.left.trans (min_le_left _ _))
            have := Nat.pow_dvd_pow_of_dvd_left (2^d.succ) (2*d.succ) (h.right.trans (min_le_right _ _))
            rw [Nat.mul_assoc, ←pow_add, ←pow_mul] at this ‹Nat.pow_dvd_pow_of_dvd_left (2 ^ d.succ) (2 * d.succ) (h.left.trans (min_le_left _ _))›
            exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left this ‹Nat.pow_dvd_pow_of_dvd_left (2 ^ d.succ) (2 * d.succ) (h.right.trans (min_le_right _ _))›) (Nat.totient_mul hcoprime)
      calc 2^(d.succ * (d.succ + 1)) = 32 * totient (2^(2^d.succ) - 1) := by rw [h1]
      ... = 2^(d.succ * (d.succ + 1)) := by
        simp only [totient, pow_succ, Nat.sub_one, totient_prime_pow, ←pow_succ, one_mul, add_sub_cancel]