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
then A2: 2 + (- 1) <= n + 0 by XREAL_1:7;
reconsider m = n - 2 as Element of NAT by A1, INT_1:5;
A3: #Z m is_differentiable_on Z by Th8, FDIFF_1:26;
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 A2, Th30
.= (((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 Th28
.= ((n * (n - 1)) (#) ((n - 2) (#) (#Z (n - 3)))) | Z by RFUNCT_1:49
.= (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z by RFUNCT_1:17 ;
hence (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z ; :: thesis: verum