English
Let x ∈ ℝ and n ∈ ℕ. If x^n ∈ ℤ and for some prime p the multiplicity of p in the factorization of x^n is not divisible by n, then x is irrational.
Русский
Пусть x ∈ ℝ и n ∈ ℕ. Если x^n ∈ ℤ и найдётся простое p such that степень p в факторизации x^n не делится на n, то x иррационально.
LaTeX
$$$x^n \in \mathbb{Z} \land \exists p\text{ prime}, \operatorname{multiplicity}(p, x^n) \not\equiv 0 \pmod{n} \Rightarrow \mathrm{Irrational}(x)$$$
Lean4
/-- If `x^n = m` is an integer and `n` does not divide the `multiplicity p m`, then `x`
is irrational. -/
theorem irrational_nrt_of_n_not_dvd_multiplicity {x : ℝ} (n : ℕ) {m : ℤ} (hm : m ≠ 0) (p : ℕ) [hp : Fact p.Prime]
(hxr : x ^ n = m) (hv : multiplicity (p : ℤ) m % n ≠ 0) : Irrational x :=
by
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
· rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
simp [hxr,
multiplicity_of_one_right (mt isUnit_iff_dvd_one.1 (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv
refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos
rintro ⟨y, rfl⟩
rw [← Int.cast_pow, Int.cast_inj] at hxr
subst m
have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl
rw [(Int.finiteMultiplicity_iff.2 ⟨by simp [hp.1.ne_one], this⟩).multiplicity_pow (Nat.prime_iff_prime_int.1 hp.1),
Nat.mul_mod_right] at hv
exact hv rfl
