α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n => x ^ n / ↑n !
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
⊢ Summable fun n => x ^ n / ↑n !
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n => x ^ n / ↑n !
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n => x ^ n / ↑n !
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 := (div_lt_one A).2 (Nat.lt_floor_add_one _)
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
this : ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
⊢ Summable fun n => x ^ n / ↑n !

case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n => x ^ n / ↑n !
suffices : ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (n + 1)!‖ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
this : ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
⊢ Summable fun n => x ^ n / ↑n !

case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
exact summable_of_ratio_norm_eventually_le B (eventually_atTop.2 ⟨⌊‖x‖⌋₊, this⟩)
case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
intro n hn
no goals
case this
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
calc
  ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
    rw [_root_.pow_succ, Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
      norm_div, Real.norm_coe_nat, Nat.cast_succ]
  _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ :=
    mul_le_mul_of_nonneg_right
      (div_le_div (norm_nonneg x) (le_refl ‖x‖) A (add_le_add (mono_cast hn) (le_refl 1)))
      (norm_nonneg (x ^ n / n !))
no goals
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
⊢ 1 ≤ ↑⌊‖x‖⌋₊ + 1
simp
no goals
α : Type ?u.2025885
β : Type ?u.2025888
ι : Type ?u.2025891
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
rw [_root_.pow_succ, Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
  norm_div, Real.norm_coe_nat, Nat.cast_succ]