no goals
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
⊢ ↑abs z / ↑n < 1
rwa [div_lt_iff hn0, one_mul]
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ↑abs z / ↑(Nat.succ m) * ↑abs (z ^ m / ↑(Nat.factorial m)) ≤ ↑abs z / ↑n * ↑abs (z ^ m / ↑(Nat.factorial m))
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ abs' (↑abs (z ^ Nat.succ m / ↑(Nat.factorial (Nat.succ m)))) ≤ ↑abs z / ↑n * abs' (↑abs (z ^ m / ↑(Nat.factorial m)))
rw [abs_abs, abs_abs, Nat.factorial_succ, pow_succ, mul_comm m.succ, Nat.cast_mul, ← div_div,
  mul_div_assoc, mul_div_right_comm, map_mul, map_div₀, abs_cast_nat]
case h.h.h
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ n ≤ Nat.succ m
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ↑abs z / ↑(Nat.succ m) * ↑abs (z ^ m / ↑(Nat.factorial m)) ≤ ↑abs z / ↑n * ↑abs (z ^ m / ↑(Nat.factorial m))
gcongr
no goals
case h.h.h
z : ℂ
n : ℕ
hn : ↑abs z < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ n ≤ Nat.succ m
exact le_trans hm (Nat.le_succ _)