let n be Nat; :: thesis: for x being Real holds

( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

let x be Real; :: thesis: ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

defpred S_{1}[ Nat] means for x being Real holds

( #Z $1 is_differentiable_in x & diff ((#Z $1),x) = $1 * (x #Z ($1 - 1)) );

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[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

( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

let x be Real; :: thesis: ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )

defpred S

( #Z $1 is_differentiable_in x & diff ((#Z $1),x) = $1 * (x #Z ($1 - 1)) );

A1: for k being Nat st S

S

proof

A4: REAL c= dom (#Z 1) by FUNCT_2:def 1;

then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:23;

A6: for x being Real holds

( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;

A15:
SA2: now :: thesis: for x being Real st x in REAL holds

(#Z 1) . x = (1 * x) + 0

A3:
[#] REAL is open Subset of REAL
;(#Z 1) . x = (1 * x) + 0

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:35 ; :: thesis: verum

end;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:35 ; :: thesis: verum

A4: REAL c= dom (#Z 1) by FUNCT_2:def 1;

then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:23;

A6: for x being Real holds

( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )

proof

let k be Nat; :: thesis: ( S
let x be Real; :: thesis: ( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )

A7: x in REAL by XREAL_0:def 1;

hence #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:9; :: thesis: diff ((#Z 1),x) = 1

thus diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by A5, A7, FDIFF_1:def 7

.= 1 by A2, A4, A3, A7, FDIFF_1:23 ; :: thesis: verum

end;A7: x in REAL by XREAL_0:def 1;

hence #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:9; :: thesis: diff ((#Z 1),x) = 1

thus diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by A5, A7, FDIFF_1:def 7

.= 1 by A2, A4, A3, A7, FDIFF_1:23 ; :: thesis: verum

assume A8: S

now :: thesis: ( ( k = 0 & S_{1}[k + 1] ) or ( k <> 0 & ( for x being Real holds

( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) ) ) )end;

hence
S( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) ) ) )

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

end;

case A9:
k = 0
; :: thesis: S_{1}[k + 1]

thus
S_{1}[k + 1]
:: thesis: verum

end;proof

let x be Real; :: 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:34 ; :: thesis: verum

end;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:34 ; :: thesis: verum

case
k <> 0
; :: thesis: for x being Real holds

( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )

( #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:13;

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;

let x be Real; :: 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;

A12: for x being object st x in dom (#Z (k + 1)) holds

(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)

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:16; :: 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:16

.= (((#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;then 1 - 1 <= k - 1 by XREAL_1:13;

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;

let x be Real; :: 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;

A12: for x being object st x in dom (#Z (k + 1)) holds

(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)

proof

A13:
#Z 1 is_differentiable_in x
by A6;
let x be object ; :: 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;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

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:16; :: 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:16

.= (((#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

proof

for n being Nat holds S
let x be Real; :: thesis: ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) )

set f = #Z 0;

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:11;

A24: x in REAL by XREAL_0:def 1;

then ((#Z 0) `| (dom (#Z 0))) . x = 0 by A21, A22, FDIFF_1:11;

hence ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:9, FDIFF_1:def 7; :: thesis: verum

end;set f = #Z 0;

now :: thesis: for y being object st y in {1} holds

y in rng (#Z 0)

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

dom (#Z 0) = REAL
by FUNCT_2:def 1;

then consider x being object such that

A16: x in dom (#Z 0) by XBOOLE_0:def 1;

reconsider x1 = x as Real by A16;

let y be object ; :: 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:34

.= y by A17, TARSKI:def 1 ;

hence y in rng (#Z 0) by A16, FUNCT_1:def 3; :: thesis: verum

end;then consider x being object such that

A16: x in dom (#Z 0) by XBOOLE_0:def 1;

reconsider x1 = x as Real by A16;

let y be object ; :: 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:34

.= y by A17, TARSKI:def 1 ;

hence y in rng (#Z 0) by A16, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for y being object st y in rng (#Z 0) holds

y in {1}

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

let y be object ; :: thesis: ( y in rng (#Z 0) implies y in {1} )

assume y in rng (#Z 0) ; :: thesis: y in {1}

then consider x being object such that

A19: x in dom (#Z 0) and

A20: y = (#Z 0) . x by FUNCT_1:def 3;

reconsider x = x as Real by A19;

(#Z 0) . x = x #Z 0 by Def1

.= 1 by PREPOWER:34 ;

hence y in {1} by A20, TARSKI:def 1; :: thesis: verum

end;assume y in rng (#Z 0) ; :: thesis: y in {1}

then consider x being object such that

A19: x in dom (#Z 0) and

A20: y = (#Z 0) . x by FUNCT_1:def 3;

reconsider x = x as Real by A19;

(#Z 0) . x = x #Z 0 by Def1

.= 1 by PREPOWER:34 ;

hence y in {1} by A20, TARSKI:def 1; :: thesis: verum

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:11;

A24: x in REAL by XREAL_0:def 1;

then ((#Z 0) `| (dom (#Z 0))) . x = 0 by A21, A22, FDIFF_1:11;

hence ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:9, FDIFF_1:def 7; :: thesis: verum

hence ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) ; :: thesis: verum