[GOAL]
m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable fun i => 1 / m ^ (i + (k + 1))!
[PROOFSTEP]
convert (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)
[GOAL]
m : ℝ
hm : 1 < m
k x✝ : ℕ
⊢ 0 ≤ 1 / m ^ (x✝ + (k + 1))!
[PROOFSTEP]
positivity
[GOAL]
m : ℝ
hm : 1 < m
k : ℕ
⊢ 0 < 1 / m ^ (0 + (k + 1))!
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ ∑' (i : ℕ), 1 / m ^ (i + (n + 1)!) = ∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!)
[PROOFSTEP]
simp only [pow_add, one_div, mul_inv, inv_pow]
  -- factor the constant `(1 / m ^ (n + 1)!)` out of the series
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
[PROOFSTEP]
rw [tsum_geometric_of_lt_1 (by positivity) mi]
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ 0 ≤ 1 / m
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 ≤ 1 / m ^ (n + 1)!
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)
[PROOFSTEP]
apply (div_le_div_iff _ _).mpr
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
conv_rhs =>
  rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
  -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
refine'
  (mul_le_mul_right _).mpr
    _
      -- solve all the inequalities `0 < m ^ ??`
[GOAL]
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
any_goals
  exact
    pow_pos (zero_lt_two.trans_le hm)
      _
        -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
[PROOFSTEP]
exact _root_.trans (_root_.trans hm (pow_one _).symm.le) (pow_mono (one_le_two.trans hm) n.factorial_pos)
[GOAL]
m : ℕ
hm : 0 < m
k : ℕ
⊢ ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
[PROOFSTEP]
induction' k with k h
[GOAL]
case zero
m : ℕ
hm : 0 < m
⊢ ∃ p, partialSum (↑m) Nat.zero = ↑p / ↑(m ^ Nat.zero !)
[PROOFSTEP]
exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]⟩
[GOAL]
m : ℕ
hm : 0 < m
⊢ partialSum (↑m) Nat.zero = ↑1 / ↑(m ^ Nat.zero !)
[PROOFSTEP]
rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]
[GOAL]
case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
rcases h with ⟨p_k, h_k⟩
[GOAL]
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
use p_k * m ^ ((k + 1)! - k !) + 1
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (Nat.succ k) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (Nat.succ k)!) + ↑(m ^ k !) * 1 * ↑(m ^ (Nat.succ k)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)
[PROOFSTEP]
norm_cast
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (Nat.succ k)! + m ^ k ! * 1 * m ^ (Nat.succ k)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
[PROOFSTEP]
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0
case h.hd m : ℕ hm : 0 < m k p_k : ℕ h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !) ⊢ ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
all_goals positivity
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
positivity
[GOAL]
m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
have mZ1 : 1 < (m : ℤ) := by norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
⊢ 1 < ↑m
[PROOFSTEP]
norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
have m1 : 1 < (m : ℝ) := by norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ 1 < ↑m
[PROOFSTEP]
norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
intro n
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
[GOAL]
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 ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
refine' ⟨p, m ^ n !, by rw [Nat.cast_pow]; exact one_lt_pow mZ1 n.factorial_ne_zero, _⟩
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑(m ^ n !)
[PROOFSTEP]
rw [Nat.cast_pow]
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑m ^ n !
[PROOFSTEP]
exact one_lt_pow mZ1 n.factorial_ne_zero
[GOAL]
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 !) ∧ |liouvilleNumber ↑m - ↑↑p / ↑↑(m ^ n !)| < 1 / ↑↑(m ^ n !) ^ n
[PROOFSTEP]
push_cast
[GOAL]
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 ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
rw [Nat.cast_pow] at hp 
[GOAL]
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 ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
rw [← partialSum_add_remainder m1 n, ← hp]
[GOAL]
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 ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
have hpos := remainder_pos m1 n
[GOAL]
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 ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)
[GOAL]
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
[PROOFSTEP]
assumption_mod_cast
