let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st n >= 2 holds
(diff (#Z n),Z) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z
let Z be open Subset of REAL ; :: thesis: ( n >= 2 implies (diff (#Z n),Z) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z )
assume A1: 2 <= n ; :: thesis: (diff (#Z n),Z) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z
A2: 2 + (- 1) <= n + 0 by A1, XREAL_1:9;
reconsider m = n - 2 as Element of NAT by A1, INT_1:18;
A3: #Z m is_differentiable_on Z by Th18, FDIFF_1:34;
then A4: ((m + 2) * (m + 1)) (#) (#Z m) is_differentiable_on Z by FDIFF_2:19;
(diff (#Z n),Z) . 3 = (diff (#Z n),Z) . (2 + 1)
.= ((diff (#Z n),Z) . 2) `| Z by TAYLOR_1:def 5
.= (((n * (n - 1)) (#) (#Z (n - 2))) | Z) `| Z by Th21, A2
.= (((m + 2) * (m + 1)) (#) (#Z m)) `| Z by A4, FDIFF_2:16
.= ((m + 2) * (m + 1)) (#) ((#Z m) `| Z) by A3, FDIFF_2:19
.= ((m + 2) * (m + 1)) (#) ((m (#) (#Z (m - 1))) | Z) by Th19
.= ((n * (n - 1)) (#) ((n - 2) (#) (#Z (n - 3)))) | Z by RFUNCT_1:65
.= (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z by RFUNCT_1:29 ;
hence (diff (#Z n),Z) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z ; :: thesis: verum