let n, m be Element of NAT ; 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; ( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z )
defpred S1[ Nat] means ( n > $1 implies (diff ((#Z n),Z)) . $1 = (((n choose $1) * ($1 !)) (#) (#Z (n - $1))) | Z );
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
assume A3:
n > k + 1
;
(diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z
then A4:
n - k > (k + 1) - k
by XREAL_1:9;
A5:
(k + 1) + (- 1) <= n + 0
by A3, XREAL_1:7;
then reconsider l =
n - k as
Element of
NAT by INT_1:5;
l >= (k + 1) - k
by A3, XREAL_1:9;
then A6:
(
(k + 1) ! > 0 &
l -' 1
= (n - k) - 1 )
by XREAL_1:233;
reconsider s =
n - (k + 1) as
Element of
NAT by A3, INT_1:5;
A7:
#Z l is_differentiable_on Z
by Th8, FDIFF_1:26;
then A8:
((n choose k) * (k !)) (#) (#Z l) is_differentiable_on Z
by FDIFF_2:19;
0 + k < 1
+ k
by XREAL_1:6;
then (diff ((#Z n),Z)) . (k + 1) =
((((n choose k) * (k !)) (#) (#Z l)) | Z) `| Z
by A2, A3, TAYLOR_1:def 5, XXREAL_0:2
.=
(((n choose k) * (k !)) (#) (#Z l)) `| Z
by A8, FDIFF_2:16
.=
((n choose k) * (k !)) (#) ((#Z l) `| Z)
by A7, 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:49
.=
((((n choose k) * (k !)) * l) (#) (#Z (l - 1))) | Z
by RFUNCT_1:17
.=
(((((n !) / ((k !) * (l !))) * (k !)) * (n - k)) (#) (#Z (l - 1))) | Z
by A5, NEWTON:def 3
.=
((((n !) / (l !)) * l) (#) (#Z (l - 1))) | Z
by XCMPLX_1:92
.=
(((n !) / ((l -' 1) !)) (#) (#Z (l - 1))) | Z
by A4, Lm1
.=
((((n !) / ((s !) * ((k + 1) !))) * ((k + 1) !)) (#) (#Z ((n - k) - 1))) | Z
by A6, XCMPLX_1:92
.=
(((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z
by A3, NEWTON:def 3
;
hence
(diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z
;
verum
end;
A9:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A9, A1);
hence
( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z )
; verum