m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber ↑m)
have mZ1 : 1 < (m : ℤ) := by norm_cast
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
have m1 : 1 < (m : ℝ) := by norm_cast
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ abs (liouvilleNumber ↑m - ↑a / ↑b) < 1 / ↑b ^ n
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
intro n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ abs (liouvilleNumber ↑m - ↑a / ↑b) < 1 / ↑b ^ n
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ abs (liouvilleNumber ↑m - ↑a / ↑b) < 1 / ↑b ^ n
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑↑p / ↑↑(m ^ n !) ∧ abs (liouvilleNumber ↑m - ↑↑p / ↑↑(m ^ n !)) < 1 / ↑↑(m ^ n !) ^ n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ abs (liouvilleNumber ↑m - ↑a / ↑b) < 1 / ↑b ^ n
refine' ⟨p, m ^ n !, by rw [Nat.cast_pow]; exact one_lt_pow mZ1 n.factorial_ne_zero, _⟩
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ abs (liouvilleNumber ↑m - ↑p / ↑m ^ n !) < 1 / (↑m ^ n !) ^ n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑↑p / ↑↑(m ^ n !) ∧ abs (liouvilleNumber ↑m - ↑↑p / ↑↑(m ^ n !)) < 1 / ↑↑(m ^ n !) ^ n
push_cast
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ abs (liouvilleNumber ↑m - ↑p / ↑m ^ n !) < 1 / (↑m ^ n !) ^ n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ abs (liouvilleNumber ↑m - ↑p / ↑m ^ n !) < 1 / (↑m ^ n !) ^ n
rw [Nat.cast_pow] at hp
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    abs (partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n) < 1 / (↑m ^ n !) ^ n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ abs (liouvilleNumber ↑m - ↑p / ↑m ^ n !) < 1 / (↑m ^ n !) ^ n
rw [← partialSum_add_remainder m1 n, ← hp]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    abs (partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n) < 1 / (↑m ^ n !) ^ n
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    abs (partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n) < 1 / (↑m ^ n !) ^ n
have hpos := remainder_pos m1 n
no goals
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    abs (partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n) < 1 / (↑m ^ n !) ^ n
simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)
no goals
m : ℕ
hm : 2 ≤ m
⊢ 1 < ↑m
norm_cast
no goals
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ 1 < ↑m
norm_cast
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑m ^ n !
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑(m ^ n !)
rw [Nat.cast_pow]
no goals
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑m ^ n !
exact one_lt_pow mZ1 n.factorial_ne_zero
no goals
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ 2 ≤ ↑m
assumption_mod_cast