Theory powser

⊢ ∀c. diffs c = (λn. &SUC n * c (SUC n))

⊢ ∀c x.
    summable (λn. diffs c n * x pow n) ⇒
    (λn. &n * (c n * x pow (n − 1))) sums suminf (λn. diffs c n * x pow n)

⊢ ∀n c x.
    sum (0,n) (λn. diffs c n * x pow n) =
    sum (0,n) (λn. &n * (c n * x pow (n − 1))) + &n * (c n * x pow (n − 1))

⊢ ∀n c x.
    sum (0,n) (λn. &n * (c n * x pow (n − 1))) =
    sum (0,n) (λn. diffs c n * x pow n) − &n * (c n * x pow (n − 1))

⊢ ∀c. diffs (λn. -c n) = (λn. -diffs c n)

⊢ ∀n x y.
    x pow SUC n − y pow SUC n =
    (x − y) * sum (0,SUC n) (λp. x pow p * y pow (n − p))

⊢ ∀n x y.
    sum (0,SUC n) (λp. x pow p * y pow (SUC n − p)) =
    y * sum (0,SUC n) (λp. x pow p * y pow (n − p))

⊢ ∀n x y.
    sum (0,SUC n) (λp. x pow p * y pow (n − p)) =
    sum (0,SUC n) (λp. x pow (n − p) * y pow p)

⊢ ∀f x z.
    summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
    summable (λn. f n * z pow n)

⊢ ∀f x z.
    summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
    summable (λn. abs (f n) * z pow n)

⊢ ∀c k' x.
    summable (λn. c n * k' pow n) ∧ summable (λn. diffs c n * k' pow n) ∧
    summable (λn. diffs (diffs c) n * k' pow n) ∧ abs x < abs k' ⇒
    ((λx. suminf (λn. c n * x pow n)) diffl
     suminf (λn. diffs c n * x pow n)) x

⊢ ∀m z h.
    sum (0,m) (λp. (z + h) pow (m − p) * z pow p − z pow m) =
    sum (0,m) (λp. z pow p * ((z + h) pow (m − p) − z pow (m − p)))

⊢ ∀z h n.
    h ≠ 0 ⇒
    ((z + h) pow n − z pow n) / h − &n * z pow (n − 1) =
    h *
    sum (0,n − 1)
      (λp.
           z pow p *
           sum (0,n − 1 − p) (λq. (z + h) pow q * z pow (n − 2 − p − q)))

⊢ ∀z h n k'.
    h ≠ 0 ∧ abs z ≤ k' ∧ abs (z + h) ≤ k' ⇒
    abs (((z + h) pow n − z pow n) / h − &n * z pow (n − 1)) ≤
    &n * (&(n − 1) * (k' pow (n − 2) * abs h))

⊢ ∀f k' k.
    0 < k ∧ (∀h. 0 < abs h ∧ abs h < k ⇒ abs (f h) ≤ k' * abs h) ⇒
    (f -> 0) 0

⊢ ∀f g k.
    0 < k ∧ summable f ∧
    (∀h. 0 < abs h ∧ abs h < k ⇒ ∀n. abs (g h n) ≤ f n * abs h) ⇒
    ((λh. suminf (g h)) -> 0) 0