English
Let x ∈ ℝ and n > 0. If x^n is an integer and x^n is not an nth power of any integer, then x is irrational.
Русский
Пусть x ∈ ℝ и n > 0. Если x^n ∈ ℤ и x^n не равняется ни степени n-й степени целого числа, то x иррационально.
LaTeX
$$$0 < n \Rightarrow x^n \in \mathbb{Z} \land \nexists y \in \mathbb{Z}, x^n = y^n \Rightarrow x \notin \mathbb{Q}$$$
Lean4
/-- If `x^n`, `n > 0`, is integer and is not the `n`-th power of an integer, then
`x` is irrational. -/
theorem irrational_nrt_of_notint_nrt {x : ℝ} (n : ℕ) (m : ℤ) (hxr : x ^ n = m) (hv : ¬∃ y : ℤ, x = y) (hnpos : 0 < n) :
Irrational x := by
rintro ⟨⟨N, D, P, C⟩, rfl⟩
rw [← cast_pow] at hxr
have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
rw [Int.cast_ne_zero, Int.natCast_ne_zero]
exact P
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
rw [mk'_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow, ← Int.cast_pow, ←
Int.cast_mul, Int.cast_inj] at hxr
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
rw [← Int.dvd_natAbs, ← Int.natCast_pow, Int.natCast_dvd_natCast, Int.natAbs_pow,
Nat.pow_dvd_pow_iff hnpos.ne'] at hdivn
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
refine hv ⟨N, ?_⟩
rw [mk'_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]
