[GOAL]
x : ℝ
⊢ LiouvilleWith 1 x
[PROOFSTEP]
use 2
[GOAL]
case h
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
have hn' : (0 : ℝ) < n := by simpa
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
[PROOFSTEP]
simpa
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by rw [lt_div_iff hn', Int.cast_add, Int.cast_one]; exact Int.lt_floor_add_one _
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x < ↑(⌊x * ↑n⌋ + 1) / ↑n
[PROOFSTEP]
rw [lt_div_iff hn', Int.cast_add, Int.cast_one]
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
exact Int.lt_floor_add_one _
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ |x - ↑(⌊x * ↑n⌋ + 1) / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add', add_div_eq_mul_add_div _ _ hn'.ne',
  div_lt_div_right hn']
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) < x * ↑n + 2
[PROOFSTEP]
convert add_lt_add_right ((Int.floor_le (x * n)).trans_lt (lt_add_one _)) 1 using 1
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
try push_cast
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
try push_cast
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑⌊x * ↑n⌋ + 1 = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
ring
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
rcases h with ⟨C, hC⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
[PROOFSTEP]
refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < max C 1 / ↑x_1 ^ p
[PROOFSTEP]
rintro n ⟨hle, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
[PROOFSTEP]
refine ⟨hle, m, hne, hlt.trans_le ?_⟩
[GOAL]
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ max C 1 / ↑n ^ p
[PROOFSTEP]
exact div_le_div_of_le (rpow_nonneg_of_nonneg n.cast_nonneg _) (le_max_left _ _)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
⊢ LiouvilleWith q x
[PROOFSTEP]
rcases h.exists_pos with ⟨C, hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith q x
[PROOFSTEP]
refine ⟨C, hC.mono ?_⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q
[PROOFSTEP]
rintro n ⟨hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ q
[PROOFSTEP]
refine ⟨m, hne, hlt.trans_le <| div_le_div_of_le_left hC₀.le ?_ ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 0 < ↑n ^ q
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑n ^ q ≤ ↑n ^ p
[PROOFSTEP]
exacts [rpow_pos_of_pos (Nat.cast_pos.2 hn) _, rpow_le_rpow_of_exponent_le (Nat.one_le_cast.2 hn) hle]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
have : ∀ᶠ n : ℕ in atTop, C < n ^ (p - q) := by
  simpa only [(· ∘ ·), neg_sub, one_div] using
    ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_nat_cast_atTop_atTop).eventually (eventually_gt_atTop C)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
[PROOFSTEP]
simpa only [(· ∘ ·), neg_sub, one_div] using
  ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_nat_cast_atTop_atTop).eventually (eventually_gt_atTop C)
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
refine (this.and_frequently hC).mono ?_
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∀ (x_1 : ℕ),
    (C < ↑x_1 ^ (p - q) ∧ 1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-q)
[PROOFSTEP]
rintro n ⟨hnC, hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
refine ⟨m, hne, hlt.trans <| (div_lt_iff <| rpow_pos_of_pos hn _).2 ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ C < ↑n ^ (-q) * ↑n ^ p
[PROOFSTEP]
rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
⊢ LiouvilleWith p (x * ↑r)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (x * ↑r)
[PROOFSTEP]
refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m,
        x * ↑r ≠ ↑m / ↑(r.den • id x_1) ∧
          |x * ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id x_1) ^ p
[PROOFSTEP]
rintro n ⟨_hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
have A : (↑(r.num * m) : ℝ) / ↑(r.den • id n) = m / n * r := by simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
[PROOFSTEP]
simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨r.num * m, ?_, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑(r.num * m) / ↑(r.den • id n)
[PROOFSTEP]
rw [A]
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑m / ↑n * ↑r
[PROOFSTEP]
simp [hne, hr]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x * ↑r - ↑(r.num * m) / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
rw [A, ← sub_mul, abs_mul]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
simp only [smul_eq_mul, id.def, Nat.cast_mul]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p
[PROOFSTEP]
refine (mul_lt_mul_of_pos_right hlt <| abs_pos.2 <| Rat.cast_ne_zero.2 hr).trans_le ?_
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ C / ↑n ^ p * |↑r| ≤ ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p
[PROOFSTEP]
rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |↑r| * (C / ↑n ^ p) ≤ ↑|r| * (C / ↑n ^ p)
[PROOFSTEP]
simp only [Rat.cast_abs, le_refl]
[GOAL]
case intro.intro.intro.intro.intro.refine_2.hc
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ↑r.den ^ p ≠ 0
[PROOFSTEP]
exact (rpow_pos_of_pos (Nat.cast_pos.2 r.pos) _).ne'
[GOAL]
case intro.intro.intro.intro.intro.refine_2.h
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑r.den
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
case intro.intro.intro.intro.intro.refine_2.h₁
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x
[PROOFSTEP]
simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel hr, Rat.cast_one, mul_one] using h.mul_rat (inv_ne_zero hr)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hr : r ≠ 0
⊢ LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_rat_iff hr]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hm : m ≠ 0
⊢ LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int, mul_rat_iff (Int.cast_ne_zero.2 hm)]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hm : m ≠ 0
⊢ LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_int_iff hm]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat, mul_rat_iff (Nat.cast_ne_zero.2 hn)]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_nat_iff hn]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)
[PROOFSTEP]
exact h.mul_nat hn
[GOAL]
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + ↑r)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (x + ↑r)
[PROOFSTEP]
refine ⟨r.den ^ p * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
[GOAL]
case intro.intro
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id x_1) ∧ |x + ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * C / ↑(r.den • id x_1) ^ p
[PROOFSTEP]
rintro n ⟨hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have hr : (0 : ℝ) < r.den := Nat.cast_pos.2 r.pos
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 (zero_lt_one.trans_le hn).ne'
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r :=
  by
  rw [Algebra.id.smul_eq_mul, id.def]
  nth_rewrite 4 [← Rat.num_div_den r]
  push_cast
  rw [add_div, mul_div_mul_left _ _ (ne_of_gt hr), mul_div_mul_right _ _ hn']
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
[PROOFSTEP]
rw [Algebra.id.smul_eq_mul, id.def]
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den * n) = ↑m / ↑n + ↑r
[PROOFSTEP]
nth_rewrite 4 [← Rat.num_div_den r]
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den * n) = ↑m / ↑n + ↑(↑r.num / ↑r.den)
[PROOFSTEP]
push_cast
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ (↑r.den * ↑m + ↑r.num * ↑n) / (↑r.den * ↑n) = ↑m / ↑n + ↑r.num / ↑r.den
[PROOFSTEP]
rw [add_div, mul_div_mul_left _ _ (ne_of_gt hr), mul_div_mul_right _ _ hn']
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨r.den * m + r.num * n, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) ∧
    |x + ↑r - ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
rw [this, add_sub_add_right_eq_sub]
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r ∧ |x - ↑m / ↑n| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have : (r.den ^ p : ℝ) ≠ 0 := (rpow_pos_of_pos hr _).ne'
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this✝ : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
this : ↑r.den ^ p ≠ 0
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
simp [mul_rpow, Nat.cast_nonneg, mul_div_mul_left, this]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p (x + ↑r)
⊢ LiouvilleWith p x
[PROOFSTEP]
simpa using h.add_rat (-r)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int m, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_int_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat n, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_nat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)
[PROOFSTEP]
rcases h with ⟨C, hC⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (-x)
[PROOFSTEP]
refine ⟨C, hC.mono ?_⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p
[PROOFSTEP]
rintro n ⟨m, hne, hlt⟩
[GOAL]
case intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ |-x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
refine ⟨-m, by simp [neg_div, hne], ?_⟩
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -x ≠ ↑(-m) / ↑n
[PROOFSTEP]
simp [neg_div, hne]
[GOAL]
case intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| < C / ↑n ^ p
[PROOFSTEP]
convert hlt using 1
[GOAL]
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| = |x - ↑m / ↑n|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |↑(-m) / ↑n - -x| = |x - ↑m / ↑n|
[PROOFSTEP]
congr! 1
[GOAL]
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n
[PROOFSTEP]
ring
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int, sub_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat, sub_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
m : ℤ
⊢ x ≠ ↑m
[PROOFSTEP]
rintro rfl
[GOAL]
p q y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False
[PROOFSTEP]
rename' m => M
[GOAL]
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False
[PROOFSTEP]
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 : ℝ)⟩
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ False
[PROOFSTEP]
refine hlt.not_le ?_
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|
[PROOFSTEP]
have hn' : (0 : ℝ) < n := by simpa
[GOAL]
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ 0 < ↑n
[PROOFSTEP]
simpa
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|
[PROOFSTEP]
rw [rpow_neg_one, ← one_div, sub_div' _ _ _ hn'.ne', abs_div, Nat.abs_cast, div_le_div_right hn']
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |↑M * ↑n - ↑m|
[PROOFSTEP]
norm_cast
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |M * ↑n - m|
[PROOFSTEP]
rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
[PROOFSTEP]
rw [Ne.def, eq_div_iff hn'.ne'] at hne 
[GOAL]
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 : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
[PROOFSTEP]
exact_mod_cast hne
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | h0)
[GOAL]
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False
[PROOFSTEP]
refine h.ne_cast_int hp 0 ?_
[GOAL]
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
[PROOFSTEP]
rw [Rat.cast_zero, Int.cast_zero]
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False
[PROOFSTEP]
refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1
[PROOFSTEP]
rw [Rat.cast_inv, mul_inv_cancel]
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1
case intro.inr p q y : ℝ r✝ : ℚ m : ℤ n : ℕ hp : 1 < p r : ℚ h : LiouvilleWith p ↑r h0 : r ≠ 0 ⊢ ↑r ≠ 0
[PROOFSTEP]
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
refine Classical.not_not.1 fun H => ?_
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
H : ¬∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
⊢ False
[PROOFSTEP]
simp only [Liouville, not_forall, not_exists, not_frequently, not_and, not_lt, eventually_atTop] at H 
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
H : ∃ a, ∀ (b : ℕ), b ≥ a → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ False
[PROOFSTEP]
rcases H with ⟨N, hN⟩
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ False
[PROOFSTEP]
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
  by
  intro b hb
  replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
  have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) :=
    by
    simp only [one_div]
    exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
  refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
  exact fun m hm a => hm a
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
intro b hb
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : b > 1
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) :=
  by
  simp only [one_div]
  exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
[PROOFSTEP]
simp only [one_div]
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => (↑b ^ m)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ), (∀ (m : ℤ), 1 / ↑b ^ x_1 ≤ dist x (↑m / ↑b)) → ∀ (a : ℤ), 1 / ↑b ^ x_1 ≤ |x - ↑a / ↑b|
[PROOFSTEP]
exact fun m hm a => hm a
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
[PROOFSTEP]
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
  (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
[PROOFSTEP]
rcases(this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩
[GOAL]
case intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
⊢ False
[PROOFSTEP]
rcases hx m with ⟨a, b, hb, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a b : ℤ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
⊢ False
[PROOFSTEP]
lift b to ℕ using zero_le_one.trans hb.le
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
⊢ False
[PROOFSTEP]
norm_cast at hb 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False
[PROOFSTEP]
push_cast at hne hlt 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
⊢ False
[PROOFSTEP]
cases' le_or_lt N b with h h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
⊢ False
[PROOFSTEP]
refine' (hN b h a hne).not_lt (hlt.trans_le _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
have hb0 : (0 : ℝ) < b := zero_lt_one.trans hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
hb0 : 0 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
exact one_div_le_one_div_of_le (pow_pos hb0 _) (pow_le_pow hb.le hnm)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inr
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : b < N
⊢ False
[PROOFSTEP]
exact (hm b h hb _).not_lt hlt
[GOAL]
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x
[PROOFSTEP]
suffices : LiouvilleWith ⌈p⌉₊ x
[GOAL]
x : ℝ
hx : Liouville x
p : ℝ
this : LiouvilleWith (↑⌈p⌉₊) x
⊢ LiouvilleWith p x
case this x : ℝ hx : Liouville x p : ℝ ⊢ LiouvilleWith (↑⌈p⌉₊) x
[PROOFSTEP]
exact this.mono (Nat.le_ceil p)
[GOAL]
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
[PROOFSTEP]
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
[GOAL]
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊
[PROOFSTEP]
rintro b ⟨_hb, a, hne, hlt⟩
[GOAL]
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
[PROOFSTEP]
refine ⟨a, hne, ?_⟩
[GOAL]
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ |x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
[PROOFSTEP]
rwa [rpow_nat_cast]
[GOAL]
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
[PROOFSTEP]
refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
rcases((eventually_gt_atTop 1).and_frequently ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists with
  ⟨b, hb, a, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
exact ⟨a, b, by exact_mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑↑b| < 1 / ↑↑b ^ n
[PROOFSTEP]
simpa [rpow_neg] using hlt
