let n be natural number ; :: thesis: for x being real number holds
( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) )
let x be real number ; :: thesis: ( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) )
defpred S₁[ natural number ] means for x being real number holds
( #Z $1 is_differentiable_in x & diff (#Z $1),x = $1 * (x #Z ($1 - 1)) );
A1: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

A2: now

let x be Real; :: thesis: ( x in REAL implies (#Z 1) . x = (1 * x) + 0 )
assume x in REAL ; :: thesis: (#Z 1) . x = (1 * x) + 0
thus (#Z 1) . x = x #Z 1 by Def1
.= (1 * x) + 0 by PREPOWER:45 ; :: thesis: verum

end;

A3: [#] REAL is open Subset of REAL ;
A4: REAL c= dom (#Z 1) by FUNCT_2:def 1;
then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:31;
A6: for x being real number holds
( #Z 1 is_differentiable_in x & diff (#Z 1),x = 1 )

proof

let x be real number ; :: thesis: ( #Z 1 is_differentiable_in x & diff (#Z 1),x = 1 )
A7: x is Real by XREAL_0:def 1;
hence #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:16; :: thesis: diff (#Z 1),x = 1
thus diff (#Z 1),x = ((#Z 1) `| REAL ) . x by A5, A7, FDIFF_1:def 8
.= 1 by A2, A4, A3, A7, FDIFF_1:31 ; :: thesis: verum

end;

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now

per cases ( k = 0 or k <> 0 ) ;

case A9: k = 0 ; :: thesis: S₁[k + 1]

thus S₁[k + 1] :: thesis: verum

proof

let x be real number ; :: thesis: ( #Z (k + 1) is_differentiable_in x & diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1)) )
thus #Z (k + 1) is_differentiable_in x by A6, A9; :: thesis: diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1))
thus diff (#Z (k + 1)),x = 1 by A6, A9
.= (k + 1) * (x #Z ((k + 1) - 1)) by A9, PREPOWER:44 ; :: thesis: verum

end;

end;

case k <> 0 ; :: thesis: for x being real number holds
( #Z (k + 1) is_differentiable_in x & diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1)) )

then 1 <= k by NAT_1:14;
then 1 - 1 <= k - 1 by XREAL_1:15;
then reconsider k1 = k - 1 as Element of NAT by INT_1:16;
let x be real number ; :: thesis: ( #Z (k + 1) is_differentiable_in x & diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1)) )
A10: REAL = dom (#Z (k + 1)) by FUNCT_2:def 1;
A11: ( x is Real & #Z k is_differentiable_in x ) by A8, XREAL_0:def 1;
A12: for x being set st x in dom (#Z (k + 1)) holds
(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)

proof

let x be set ; :: thesis: ( x in dom (#Z (k + 1)) implies (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) )
assume x in dom (#Z (k + 1)) ; :: thesis: (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)
then reconsider x1 = x as Real ;
thus (#Z (k + 1)) . x = x1 #Z (k + 1) by Def1
.= (x1 #Z k) * (x1 #Z 1) by Th1
.= ((#Z k) . x) * (x1 #Z 1) by Def1
.= ((#Z k) . x) * ((#Z 1) . x) by Def1 ; :: thesis: verum

end;

A13: #Z 1 is_differentiable_in x by A6;
A14: (dom (#Z k)) /\ (dom (#Z 1)) = ([#] REAL ) /\ (dom (#Z 1)) by FUNCT_2:def 1
.= ([#] REAL ) /\ REAL by FUNCT_2:def 1 ;
then #Z (k + 1) = (#Z k) (#) (#Z 1) by A10, A12, VALUED_1:def 4;
hence #Z (k + 1) is_differentiable_in x by A11, A13, FDIFF_1:24; :: thesis: diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1))
thus diff (#Z (k + 1)),x = diff ((#Z k) (#) (#Z 1)),x by A14, A10, A12, VALUED_1:def 4
.= (((#Z k) . x) * (diff (#Z 1),x)) + ((diff (#Z k),x) * ((#Z 1) . x)) by A11, A13, FDIFF_1:24
.= (((#Z k) . x) * 1) + ((diff (#Z k),x) * ((#Z 1) . x)) by A6
.= ((x #Z k) * 1) + ((diff (#Z k),x) * ((#Z 1) . x)) by Def1
.= ((x #Z k) * 1) + ((diff (#Z k),x) * (x #Z 1)) by Def1
.= (x #Z k) + ((k * (x #Z k1)) * (x #Z 1)) by A8
.= (x #Z k) + (k * ((x #Z k1) * (x #Z 1)))
.= (x #Z k) + (k * (x #Z (k1 + 1))) by Th1
.= (k + 1) * (x #Z ((k + 1) - 1)) ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A15: S₁[ 0 ]

proof

let x be real number ; :: thesis: ( #Z 0 is_differentiable_in x & diff (#Z 0 ),x = 0 * (x #Z (0 - 1)) )
set f = #Z 0 ;

now

dom (#Z 0 ) = REAL by FUNCT_2:def 1;
then consider x being set such that
A16: x in dom (#Z 0 ) ;
reconsider x1 = x as Real by A16;
let y be set ; :: thesis: ( y in {1} implies y in rng (#Z 0 ) )
assume A17: y in {1} ; :: thesis: y in rng (#Z 0 )
(#Z 0 ) . x = x1 #Z 0 by Def1
.= 1 by PREPOWER:44
.= y by A17, TARSKI:def 1 ;
hence y in rng (#Z 0 ) by A16, FUNCT_1:def 5; :: thesis: verum

end;

then A18: {1} c= rng (#Z 0 ) by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in rng (#Z 0 ) implies y in {1} )
assume y in rng (#Z 0 ) ; :: thesis: y in {1}
then consider x being set such that
A19: x in dom (#Z 0 ) and
A20: y = (#Z 0 ) . x by FUNCT_1:def 5;
reconsider x = x as Real by A19;
(#Z 0 ) . x = x #Z 0 by Def1
.= 1 by PREPOWER:44 ;
hence y in {1} by A20, TARSKI:def 1; :: thesis: verum

end;

then rng (#Z 0 ) c= {1} by TARSKI:def 3;
then A21: rng (#Z 0 ) = {1} by A18, XBOOLE_0:def 10;
A22: dom (#Z 0 ) = [#] REAL by FUNCT_2:def 1;
then A23: #Z 0 is_differentiable_on dom (#Z 0 ) by A21, FDIFF_1:19;
A24: x is Real by XREAL_0:def 1;
then ((#Z 0 ) `| (dom (#Z 0 ))) . x = 0 by A21, A22, FDIFF_1:19;
hence ( #Z 0 is_differentiable_in x & diff (#Z 0 ),x = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:16, FDIFF_1:def 8; :: thesis: verum

end;

for n being natural number holds S₁[n] from NAT_1:sch 2(A15, A1);
hence ( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) ) ; :: thesis: verum