Two lemmas about rational power of natural number

Stream: Is there code for X?

[Ilmārs Cīrulis]

Are they in Mathlib in some form? If not, would they be good for Mathlib?
Thank you!

import Mathlib

lemma aux4 (a : ℕ) (p q : ℚ) (h : (q : ℝ) = (a : ℝ) ^ (p : ℝ)) :
    ∃ (b : ℕ), a = b ^ p.den := by sorry

lemma aux5 (a : ℕ) (p q : ℚ) (hp : 0 ≤ p) (h : (q : ℝ) = (a : ℝ) ^ (p : ℝ)) :
    ∃ (n : ℕ), (n : ℚ) = q := by sorry

[Ilmārs Cīrulis]

Their use?... For finding/proving natural number solutions for some equations that contain exponentiation, probably. At least that's where I used them.

Maybe there are some other use cases, I don't know.

[Snir Broshi]

I like these, they seem to lead to equations of the form a ^ b = c ^ d for (a b c d : ℕ), and specifically the case where Nat.Coprime b d.
Though I'm not a fan of the particular way they're stated, using rationals and reals. Can you make them only about naturals/integers?
btw I think aux5 is a single application of docs#irrational_nrt_of_notint_nrt, and its statement can be strengthened to q.den = 1.

[Ilmārs Cīrulis]

They are in such form because I wanted to reason about natural number to rational power, and that's only possible, I believe, when both base and exponent are coerced to real numbers. :thinking:

The first proof ultimately uses the nice theorem docs#Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow

[Snir Broshi]

Oh wow, merged just last week (#28557), didn't know this existed, thanks!

[Ilmārs Cīrulis]

Can you make them only about naturals/integers?

I will try to make such versions too.

[Ilmārs Cīrulis]

:partying_face: There they are, if I did everything correctly. Now they look trivial. :D

import Mathlib

lemma aux₁ {n a b c d : ℕ} (hb : b ≠ 0) (h : c ^ b = d ^ b * n ^ a) : d ∣ c := by
  have h₁ : d ^ b ∣ c ^ b := by use (n ^ a)
  exact (Nat.pow_dvd_pow_iff hb).mp h₁

lemma aux₂ (n a b c d : ℕ) (hb : b ≠ 0) (hd : d ≠ 0) (hab : a.Coprime b) (h : c ^ b = d ^ b * n ^ a) :
    ∃ (m : ℕ), n = m ^ b := by
  obtain ⟨e, rfl⟩ := aux₁ hb h
  grind [Nat.eq_of_mul_eq_mul_left, Nat.pow_pos, mul_pow,
    Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow]

[Ilmārs Cīrulis]

Hmm, maybe I can remake the proof where I used them, to use natural numbers only. :thinking:

[Snir Broshi]

Cool! Though I agree they look trivial now, maybe they can be inlined to the parent proof?

[Ilmārs Cīrulis]

Yes, that could be possible. Will try.

Thank you! :)

[Ilmārs Cīrulis]

Wow, now the proof seems like super-easy and will be soon finished. Damn you, weird human proof I formalized. :joy:

[Ilmārs Cīrulis]

Anyway, there's the parent proof, even if it is a bit off-topic. So tiny! :octopus:

import Mathlib

lemma ineq₁ {n b : ℕ} (hb : 2 ≤ b) (hn : 5 ≤ n) : n < b ^ (n - 2) := by
  induction n, hn using Nat.le_induction with
  | base => norm_num; linarith [Nat.pow_le_pow_left hb 3]
  | succ n hn iH => rw [show n + 1 - 2 = n - 2 + 1 by cutsat, Nat.pow_succ]; nlinarith

lemma ineq₂ {n b : ℕ} (hb : 2 ≤ b) (hn : 5 ≤ n) : n * b ^ 2 < b ^ n := by
  nth_rw 2 [show n = n - 2 + 2 by cutsat]
  rw [Nat.pow_add]
  nlinarith [ineq₁ hb hn]

lemma ineq₃ {x y b : ℕ} (hb : 2 ≤ b) (hxy : x < y) : b + x < b ^ 2 * y := by
  induction b, hb using Nat.le_induction <;> nlinarith

lemma ineq₄ {b : ℕ} (n : ℕ) (hb : 2 ≤ b) : b * n < (b ^ n) ^ 2 := by
  induction n with
  | zero => simp
  | succ n iH => ring_nf at *; exact ineq₃ hb iH

lemma aux₁ {n b : ℕ} (h : n * b ^ 2 = b ^ n) : b ≤ 1 ∨ n ≤ 4 := by grind [ineq₂]

lemma aux₂ {n b : ℕ} (h : b * n = (b ^ n) ^ 2) : b ≤ 1 := by grind [ineq₄]

lemma aux₃ {n a b c d : ℕ} (hb : b ≠ 0) (h : c ^ b = d ^ b * n ^ a) : d ∣ c :=
  (Nat.pow_dvd_pow_iff hb).mp (Dvd.intro (n ^ a) h.symm)

theorem T (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    a ^ (b ^ 2) = b ^ a ↔ ((a, b) = (1, 1) ∨ (a, b) = (16, 2) ∨ (a, b) = (27, 3)) := by
  constructor <;> intro H
  · by_cases h₁ : 2 * b ^ 2 ≤ a
    · have h₂ : b ^ a = (b ^ 2) ^ (b ^ 2) * b ^ (a - 2 * b ^ 2) := by
        rw [← pow_mul, ← pow_add]; congr; cutsat
      have h₃ : b ^ 2 ∣ a := by
        rw [h₂] at H
        exact aux₃ (by nlinarith) H
      obtain ⟨d, hd⟩ := h₃
      rw [hd, mul_comm, pow_mul, Nat.pow_left_inj (pow_ne_zero 2 (Nat.ne_zero_of_lt hb))] at H
      obtain h₄ | h₄ := aux₁ H
      · interval_cases b; grind
      · interval_cases d
        · simp at H
        · have h₃ : b = 1 := by nlinarith
          grind
        · nlinarith
        · have h₃ : b = 3 := by nlinarith
          grind
        · have h₃ : b = 2 := by
            rw [show b ^ 4 = b ^ 2 * b ^ 2 by ring] at H
            have h₄ : b ^ 2 = 4 := by nlinarith
            nlinarith
          grind
    · simp at h₁
      have h₂ : (b ^ 2) ^ (b ^ 2) = a ^ (b ^ 2) * b ^ (2 * b ^ 2 - a) := by
        rw [H, ← pow_add, ← pow_mul]; congr; cutsat
      have h₃ : a ∣ b ^ 2 := aux₃ (by nlinarith) h₂
      obtain ⟨d, hd⟩ := h₃
      rw [hd, mul_comm, pow_mul, Nat.pow_left_inj (Nat.ne_zero_of_lt ha)] at H
      rw [← H] at hd
      have h₄ := aux₂ hd.symm
      interval_cases a; grind
  · grind