x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
have h3 : |x| = x := by simpa
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
have h4 : |x| ≤ 1 := by rwa [h3]
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' :
  abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
have h' := Real.exp_bound h4 hn
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' :
  abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
rw [h3] at h'
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
h'' : exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
have h'' := (abs_sub_le_iff.1 h').1
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
h'' : exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
t : exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
h'' : exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
have t := sub_le_iff_le_add'.1 h''
no goals
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
h4 : abs' x ≤ 1
h' : abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
h'' : exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m) ≤ x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
t : exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
⊢ exp x ≤ ∑ m in range n, x ^ m / ↑(Nat.factorial m) + x ^ n * (↑n + 1) / (↑(Nat.factorial n) * ↑n)
simpa [mul_div_assoc] using t
no goals
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ abs' x = x
simpa
no goals
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : abs' x = x
⊢ abs' x ≤ 1
rwa [h3]