let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st n > m holds
(diff (#Z n),Z) . m = (((n choose m) * (m ! )) (#) (#Z (n - m))) | Z
let Z be open Subset of REAL ; :: thesis: ( n > m implies (diff (#Z n),Z) . m = (((n choose m) * (m ! )) (#) (#Z (n - m))) | Z )
defpred S₁[ Nat] means ( n > $1 implies (diff (#Z n),Z) . $1 = (((n choose $1) * ($1 ! )) (#) (#Z (n - $1))) | Z );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
A3: k ! > 0 by NEWTON:23;
assume A4: n > k + 1 ; :: thesis: (diff (#Z n),Z) . (k + 1) = (((n choose (k + 1)) * ((k + 1) ! )) (#) (#Z (n - (k + 1)))) | Z
then A5: n - k > (k + 1) - k by XREAL_1:11;
A6: (k + 1) + (- 1) <= n + 0 by A4, XREAL_1:9;
then reconsider l = n - k as Element of NAT by INT_1:18;
l >= (k + 1) - k by A4, XREAL_1:11;
then A7: ( (k + 1) ! > 0 & l -' 1 = (n - k) - 1 ) by NEWTON:23, XREAL_1:235;
reconsider s = n - (k + 1) as Element of NAT by A4, INT_1:18;
A8: #Z l is_differentiable_on Z by Th8, FDIFF_1:34;
then A9: ((n choose k) * (k ! )) (#) (#Z l) is_differentiable_on Z by FDIFF_2:19;
0 + k < 1 + k by XREAL_1:8;
then (diff (#Z n),Z) . (k + 1) = ((((n choose k) * (k ! )) (#) (#Z l)) | Z) `| Z by A2, A4, TAYLOR_1:def 5, XXREAL_0:2
.= (((n choose k) * (k ! )) (#) (#Z l)) `| Z by A9, FDIFF_2:16
.= ((n choose k) * (k ! )) (#) ((#Z l) `| Z) by A8, FDIFF_2:19
.= ((n choose k) * (k ! )) (#) ((l (#) (#Z (l - 1))) | Z) by Th28
.= (((n choose k) * (k ! )) (#) (l (#) (#Z (l - 1)))) | Z by RFUNCT_1:65
.= ((((n choose k) * (k ! )) * l) (#) (#Z (l - 1))) | Z by RFUNCT_1:29
.= (((((n ! ) / ((k ! ) * (l ! ))) * (k ! )) * (n - k)) (#) (#Z (l - 1))) | Z by A6, NEWTON:def 3
.= ((((n ! ) / (l ! )) * l) (#) (#Z (l - 1))) | Z by A3, XCMPLX_1:93
.= (((n ! ) / ((l -' 1) ! )) (#) (#Z (l - 1))) | Z by A5, Lm1
.= ((((n ! ) / ((s ! ) * ((k + 1) ! ))) * ((k + 1) ! )) (#) (#Z ((n - k) - 1))) | Z by A7, XCMPLX_1:93
.= (((n choose (k + 1)) * ((k + 1) ! )) (#) (#Z (n - (k + 1)))) | Z by A4, NEWTON:def 3 ;
hence (diff (#Z n),Z) . (k + 1) = (((n choose (k + 1)) * ((k + 1) ! )) (#) (#Z (n - (k + 1)))) | Z ; :: thesis: verum

end;

A10: S₁[ 0 ]

proof

assume n > 0 ; :: thesis: (diff (#Z n),Z) . 0 = (((n choose 0 ) * (0 ! )) (#) (#Z (n - 0 ))) | Z
(diff (#Z n),Z) . 0 = (#Z n) | Z by TAYLOR_1:def 5
.= ((1 * 1) (#) (#Z n)) | Z by RFUNCT_1:33
.= (((n choose 0 ) * (0 ! )) (#) (#Z (n - 0 ))) | Z by NEWTON:18, NEWTON:29 ;
hence (diff (#Z n),Z) . 0 = (((n choose 0 ) * (0 ! )) (#) (#Z (n - 0 ))) | Z ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A1);
hence ( n > m implies (diff (#Z n),Z) . m = (((n choose m) * (m ! )) (#) (#Z (n - m))) | Z ) ; :: thesis: verum