p q y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False
p q x y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
m : ℤ
⊢ x ≠ ↑m
rintro rfl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False
p q y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False
rename' m => M
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
⊢ False
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False
rcases((eventually_gt_atTop 0).and_frequently (h.frequently_lt_rpow_neg hp)).exists with
  ⟨n : ℕ, hn : 0 < n, m : ℤ, hne : (M : ℝ) ≠ m / n, hlt : |(M - m / n : ℝ)| < n ^ (-1 : ℝ)⟩
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ abs (↑M - ↑m / ↑n)
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
⊢ False
refine hlt.not_le ?_
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ abs (↑M - ↑m / ↑n)
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ abs (↑M - ↑m / ↑n)
have hn' : (0 : ℝ) < n := by simpa
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ abs (↑M * ↑n - ↑m)
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ abs (↑M - ↑m / ↑n)
rw [rpow_neg_one, ← one_div, sub_div' _ _ _ hn'.ne', abs_div, Nat.abs_cast, div_le_div_right hn']
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ abs (M * ↑n - m)
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ abs (↑M * ↑n - ↑m)
norm_cast
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ abs (M * ↑n - m)
rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬↑M * ↑n = ↑m
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
rw [Ne.def, eq_div_iff hn'.ne'] at hne
no goals
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬↑M * ↑n = ↑m
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
exact_mod_cast hne
no goals
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : abs (↑M - ↑m / ↑n) < ↑n ^ (-1)
⊢ 0 < ↑n
simpa