x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ↑(const abs' (∑ i in range n, x ^ i / ↑i !)) j ≤
    ↑{ val := fun n => (↑(exp' ↑x) n).re, property := (_ : IsCauSeq abs' fun n => (↑(exp' ↑x) n).re) } j
x✝ y x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ∑ i in range n, x ^ i / ↑i ! ≤
    CauSeq.lim { val := fun n => (↑(exp' ↑x) n).re, property := (_ : IsCauSeq abs' fun n => (↑(exp' ↑x) n).re) }
refine' le_lim (CauSeq.le_of_exists ⟨n, fun j hj => _⟩)
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤ ∑ i in range j, (↑x ^ i / ↑i !).re
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ↑(const abs' (∑ i in range n, x ^ i / ↑i !)) j ≤
    ↑{ val := fun n => (↑(exp' ↑x) n).re, property := (_ : IsCauSeq abs' fun n => (↑(exp' ↑x) n).re) } j
simp only [exp', const_apply, re_sum]
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤ ∑ i in range j, x ^ i / ↑i !
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤ ∑ i in range j, (↑x ^ i / ↑i !).re
norm_cast
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤
    ∑ x_1 in range n, x ^ x_1 / ↑x_1 ! + ∑ x_1 in range (j - n), x ^ (n + x_1) / ↑(n + x_1)!
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤ ∑ i in range j, x ^ i / ↑i !
rw [← Nat.add_sub_of_le hj, Finset.sum_range_add]
x✝¹ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
i : ℕ
x✝ : i ∈ range (j - n)
⊢ 0 ≤ x ^ (n + i) / ↑(n + i)!
x✝ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i in range n, x ^ i / ↑i ! ≤
    ∑ x_1 in range n, x ^ x_1 / ↑x_1 ! + ∑ x_1 in range (j - n), x ^ (n + x_1) / ↑(n + x_1)!
refine' le_add_of_nonneg_right (sum_nonneg fun i _ => _)
no goals
x✝¹ y x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
i : ℕ
x✝ : i ∈ range (j - n)
⊢ 0 ≤ x ^ (n + i) / ↑(n + i)!
positivity
no goals
x✝ y x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ CauSeq.lim { val := fun n => (↑(exp' ↑x) n).re, property := (_ : IsCauSeq abs' fun n => (↑(exp' ↑x) n).re) } = exp x
rw [exp, Complex.exp, ← cauSeqRe, lim_re]