let p be Real; :: thesis: for f being one-to-one PartFunc of REAL,REAL st left_open_halfline p c= dom f & f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds
diff (f,x0) < 0 ) holds
( f | (left_open_halfline p) is one-to-one & (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) ") & ( for x0 being Real st x0 in dom ((f | (left_open_halfline p)) ") holds
diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) ) )
let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( left_open_halfline p c= dom f & f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds
diff (f,x0) < 0 ) implies ( f | (left_open_halfline p) is one-to-one & (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) ") & ( for x0 being Real st x0 in dom ((f | (left_open_halfline p)) ") holds
diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) ) ) )
set l = left_open_halfline p;
assume that
left_open_halfline p c= dom f and
A1: f is_differentiable_on left_open_halfline p and
A2: ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds
diff (f,x0) < 0 ) ; :: thesis: ( f | (left_open_halfline p) is one-to-one & (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) ") & ( for x0 being Real st x0 in dom ((f | (left_open_halfline p)) ") holds
diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) ) )
A3: rng (f | (left_open_halfline p)) is open by A1, A2, Th42;
set f1 = f | (left_open_halfline p);
thus f | (left_open_halfline p) is one-to-one ; :: thesis: ( (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) ") & ( for x0 being Real st x0 in dom ((f | (left_open_halfline p)) ") holds
diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) ) )
A4: dom ((f | (left_open_halfline p)) ") = rng (f | (left_open_halfline p)) by FUNCT_1:33;
A5: rng ((f | (left_open_halfline p)) ") = dom (f | (left_open_halfline p)) by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom ((f | (left_open_halfline p)) ") holds
( (f | (left_open_halfline p)) " is_differentiable_in y0 & diff (((f | (left_open_halfline p)) "),y0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) )
proof
let y0 be Element of REAL ; :: thesis: ( y0 in dom ((f | (left_open_halfline p)) ") implies ( (f | (left_open_halfline p)) " is_differentiable_in y0 & diff (((f | (left_open_halfline p)) "),y0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) ) )
assume A7: y0 in dom ((f | (left_open_halfline p)) ") ; :: thesis: ( (f | (left_open_halfline p)) " is_differentiable_in y0 & diff (((f | (left_open_halfline p)) "),y0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) )
then consider x0 being Element of REAL such that
A8: x0 in dom (f | (left_open_halfline p)) and
A9: y0 = (f | (left_open_halfline p)) . x0 by A4, PARTFUN1:3;
A10: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {y0} & rng (h + c) c= dom ((f | (left_open_halfline p)) ") holds
( (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) is convergent & lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) )
proof
A11: left_open_halfline p c= dom f by A1;
( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A1, A2, Th29, Th30;
then ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous by A11, FCONT_3:18;
then A12: ((f | (left_open_halfline p)) ") | (rng (f | (left_open_halfline p))) is continuous by RELAT_1:115;
y0 in dom (((f | (left_open_halfline p)) ") | (rng (f | (left_open_halfline p)))) by A4, A7, RELAT_1:69;
then ((f | (left_open_halfline p)) ") | (rng (f | (left_open_halfline p))) is_continuous_in y0 by A12, FCONT_1:def 2;
then A13: (f | (left_open_halfline p)) " is_continuous_in y0 by A4, RELAT_1:68;
reconsider fy = ((f | (left_open_halfline p)) ") . y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const (((f | (left_open_halfline p)) ") . y0);
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {y0} & rng (h + c) c= dom ((f | (left_open_halfline p)) ") holds
( (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) is convergent & lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) )
let c be constant Real_Sequence; :: thesis: ( rng c = {y0} & rng (h + c) c= dom ((f | (left_open_halfline p)) ") implies ( (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) is convergent & lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) ) )
assume that
A14: rng c = {y0} and
A15: rng (h + c) c= dom ((f | (left_open_halfline p)) ") ; :: thesis: ( (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) is convergent & lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) )
A16: lim (h + c) = y0 by A14, Th4;
reconsider a = seq_const (((f | (left_open_halfline p)) ") . y0) as constant Real_Sequence ;
defpred S1[ Element of NAT , Real] means for r1, r2 being Real st r1 = (h + c) . $1 & r2 = a . $1 holds
( r1 = f . (r2 + $2) & r2 + $2 in dom f & r2 + $2 in dom (f | (left_open_halfline p)) );
A17: for n being Element of NAT ex r being Element of REAL st S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S1[n,r]
(h + c) . n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
A18: g in dom (f | (left_open_halfline p)) and
A19: (h + c) . n = (f | (left_open_halfline p)) . g by A4, A15, PARTFUN1:3;
take r = g - x0; :: thesis: S1[n,r]
let r1, r2 be Real; :: thesis: ( r1 = (h + c) . n & r2 = a . n implies ( r1 = f . (r2 + r) & r2 + r in dom f & r2 + r in dom (f | (left_open_halfline p)) ) )
assume that
A20: r1 = (h + c) . n and
A21: r2 = a . n ; :: thesis: ( r1 = f . (r2 + r) & r2 + r in dom f & r2 + r in dom (f | (left_open_halfline p)) )
A22: a . n = ((f | (left_open_halfline p)) ") . ((f | (left_open_halfline p)) . x0) by A9, SEQ_1:57
.= x0 by A8, FUNCT_1:34 ;
hence r1 = f . (r2 + r) by A18, A19, A20, A21, FUNCT_1:47; :: thesis: ( r2 + r in dom f & r2 + r in dom (f | (left_open_halfline p)) )
g in (dom f) /\ (left_open_halfline p) by A18, RELAT_1:61;
hence ( r2 + r in dom f & r2 + r in dom (f | (left_open_halfline p)) ) by A18, A22, A21, XBOOLE_0:def 4; :: thesis: verum
end;
consider b being Real_Sequence such that
A23: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch 3(A17);
A24: now :: thesis: for n being Element of NAT holds ((((f | (left_open_halfline p)) ") /* (h + c)) - a) . n = b . n
let n be Element of NAT ; :: thesis: ((((f | (left_open_halfline p)) ") /* (h + c)) - a) . n = b . n
A25: (h + c) . n = (h + c) . n ;
then A26: (a . n) + (b . n) in dom (f | (left_open_halfline p)) by A23;
thus ((((f | (left_open_halfline p)) ") /* (h + c)) - a) . n = ((((f | (left_open_halfline p)) ") /* (h + c)) . n) - (a . n) by RFUNCT_2:1
.= (((f | (left_open_halfline p)) ") . ((h + c) . n)) - (a . n) by A15, FUNCT_2:108
.= (((f | (left_open_halfline p)) ") . (f . ((a . n) + (b . n)))) - (a . n) by A23
.= (((f | (left_open_halfline p)) ") . ((f | (left_open_halfline p)) . ((a . n) + (b . n)))) - (a . n) by A23, A25, FUNCT_1:47
.= ((a . n) + (b . n)) - (a . n) by A26, FUNCT_1:34
.= b . n ; :: thesis: verum
end;
A27: ((f | (left_open_halfline p)) ") /* (h + c) is convergent by A15, A16, A13, FCONT_1:def 1;
then (((f | (left_open_halfline p)) ") /* (h + c)) - a is convergent ;
then A28: b is convergent by A24, FUNCT_2:63;
A29: lim a = a . 0 by SEQ_4:26
.= ((f | (left_open_halfline p)) ") . y0 by SEQ_1:57 ;
((f | (left_open_halfline p)) ") . y0 = lim (((f | (left_open_halfline p)) ") /* (h + c)) by A15, A16, A13, FCONT_1:def 1;
then lim ((((f | (left_open_halfline p)) ") /* (h + c)) - a) = (((f | (left_open_halfline p)) ") . y0) - (((f | (left_open_halfline p)) ") . y0) by A27, A29, SEQ_2:12
.= 0 ;
then A30: lim b = 0 by A24, FUNCT_2:63;
A31: rng (b + a) c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (b + a) or x in dom f )
assume x in rng (b + a) ; :: thesis: x in dom f
then consider n being Element of NAT such that
A32: x = (b + a) . n by FUNCT_2:113;
A33: (h + c) . n = (h + c) . n ;
x = (a . n) + (b . n) by A32, SEQ_1:7;
hence x in dom f by A23, A33; :: thesis: verum
end;
((f | (left_open_halfline p)) ") . y0 in dom (f | (left_open_halfline p)) by A5, A7, FUNCT_1:def 3;
then ((f | (left_open_halfline p)) ") . y0 in (dom f) /\ (left_open_halfline p) by RELAT_1:61;
then A34: ((f | (left_open_halfline p)) ") . y0 in left_open_halfline p by XBOOLE_0:def 4;
then A35: f is_differentiable_in ((f | (left_open_halfline p)) ") . y0 by A1, FDIFF_1:9;
A36: now :: thesis: for n being Element of NAT holds c . n = (f | (left_open_halfline p)) . x0
let n be Element of NAT ; :: thesis: c . n = (f | (left_open_halfline p)) . x0
c . n in rng c by VALUED_0:28;
hence c . n = (f | (left_open_halfline p)) . x0 by A9, A14, TARSKI:def 1; :: thesis: verum
end;
A37: 0 <> diff (f,(((f | (left_open_halfline p)) ") . y0)) by A2, A34;
now :: thesis: for n being Nat holds not b . n = 0
given n being Nat such that A38: b . n = 0 ; :: thesis: contradiction
A39: n in NAT by ORDINAL1:def 12;
a . n = ((f | (left_open_halfline p)) ") . ((f | (left_open_halfline p)) . x0) by A9, SEQ_1:57
.= x0 by A8, FUNCT_1:34 ;
then A40: f . ((a . n) + (b . n)) = (f | (left_open_halfline p)) . x0 by A8, A38, FUNCT_1:47;
(h + c) . n = (h . n) + (c . n) by SEQ_1:7
.= (h . n) + ((f | (left_open_halfline p)) . x0) by A36, A39 ;
then (h . n) + ((f | (left_open_halfline p)) . x0) = (f | (left_open_halfline p)) . x0 by A23, A40, A39;
hence contradiction by SEQ_1:5; :: thesis: verum
end;
then b is non-zero by SEQ_1:5;
then reconsider b = b as non-zero 0 -convergent Real_Sequence by A28, A30, FDIFF_1:def 1;
A41: b " is non-zero by SEQ_1:33;
A42: rng a = {(((f | (left_open_halfline p)) ") . y0)}
proof
thus rng a c= {(((f | (left_open_halfline p)) ") . y0)} :: according to XBOOLE_0:def 10 :: thesis: {(((f | (left_open_halfline p)) ") . y0)} c= rng a
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in {(((f | (left_open_halfline p)) ") . y0)} )
assume x in rng a ; :: thesis: x in {(((f | (left_open_halfline p)) ") . y0)}
then ex n being Element of NAT st x = a . n by FUNCT_2:113;
then x = ((f | (left_open_halfline p)) ") . y0 by SEQ_1:57;
hence x in {(((f | (left_open_halfline p)) ") . y0)} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(((f | (left_open_halfline p)) ") . y0)} or x in rng a )
assume x in {(((f | (left_open_halfline p)) ") . y0)} ; :: thesis: x in rng a
then x = ((f | (left_open_halfline p)) ") . y0 by TARSKI:def 1;
then a . 0 = x by SEQ_1:57;
hence x in rng a by VALUED_0:28; :: thesis: verum
end;
A43: rng a c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in dom f )
assume x in rng a ; :: thesis: x in dom f
then x = ((f | (left_open_halfline p)) ") . y0 by A42, TARSKI:def 1;
then x = x0 by A8, A9, FUNCT_1:34;
then x in (dom f) /\ (left_open_halfline p) by A8, RELAT_1:61;
hence x in dom f by XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: for n being Element of NAT holds (f /* a) . n = c . n
let n be Element of NAT ; :: thesis: (f /* a) . n = c . n
A44: ((f | (left_open_halfline p)) ") . y0 in rng ((f | (left_open_halfline p)) ") by A7, FUNCT_1:def 3;
c . n in rng c by VALUED_0:28;
then A45: c . n = y0 by A14, TARSKI:def 1;
thus (f /* a) . n = f . (a . n) by A43, FUNCT_2:108
.= f . (((f | (left_open_halfline p)) ") . y0) by SEQ_1:57
.= (f | (left_open_halfline p)) . (((f | (left_open_halfline p)) ") . y0) by A5, A44, FUNCT_1:47
.= c . n by A4, A7, A45, FUNCT_1:35 ; :: thesis: verum
end;
then A46: f /* a = c ;
now :: thesis: for n being Element of NAT holds h . n = ((f /* (b + a)) - (f /* a)) . n
let n be Element of NAT ; :: thesis: h . n = ((f /* (b + a)) - (f /* a)) . n
(h + c) . n = f . ((a . n) + (b . n)) by A23;
then (h . n) + (c . n) = f . ((a . n) + (b . n)) by SEQ_1:7;
hence h . n = (f . ((b . n) + (a . n))) - ((f /* a) . n) by A46
.= (f . ((b + a) . n)) - ((f /* a) . n) by SEQ_1:7
.= ((f /* (b + a)) . n) - ((f /* a) . n) by A31, FUNCT_2:108
.= ((f /* (b + a)) - (f /* a)) . n by RFUNCT_2:1 ;
:: thesis: verum
end;
then A47: h = (f /* (b + a)) - (f /* a) ;
then (f /* (b + a)) - (f /* a) is non-zero ;
then A48: (b ") (#) ((f /* (b + a)) - (f /* a)) is non-zero by A41, SEQ_1:35;
A49: rng c c= dom ((f | (left_open_halfline p)) ") by A7, A14, TARSKI:def 1;
now :: thesis: for n being Element of NAT holds ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) . n = (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n
let n be Element of NAT ; :: thesis: ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) . n = (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n
A50: (h + c) . n = (h + c) . n ;
then A51: (a . n) + (b . n) in dom (f | (left_open_halfline p)) by A23;
c . n in rng c by VALUED_0:28;
then A52: c . n = y0 by A14, TARSKI:def 1;
thus ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) . n = ((h ") . n) * (((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) . n) by SEQ_1:8
.= ((h ") . n) * (((((f | (left_open_halfline p)) ") /* (h + c)) . n) - ((((f | (left_open_halfline p)) ") /* c) . n)) by RFUNCT_2:1
.= ((h ") . n) * ((((f | (left_open_halfline p)) ") . ((h + c) . n)) - ((((f | (left_open_halfline p)) ") /* c) . n)) by A15, FUNCT_2:108
.= ((h ") . n) * ((((f | (left_open_halfline p)) ") . (f . ((a . n) + (b . n)))) - ((((f | (left_open_halfline p)) ") /* c) . n)) by A23
.= ((h ") . n) * ((((f | (left_open_halfline p)) ") . ((f | (left_open_halfline p)) . ((a . n) + (b . n)))) - ((((f | (left_open_halfline p)) ") /* c) . n)) by A23, A50, FUNCT_1:47
.= ((h ") . n) * (((a . n) + (b . n)) - ((((f | (left_open_halfline p)) ") /* c) . n)) by A51, FUNCT_1:34
.= ((h ") . n) * (((a . n) + (b . n)) - (((f | (left_open_halfline p)) ") . (c . n))) by A49, FUNCT_2:108
.= ((h ") . n) * (((a . n) + (b . n)) - (a . n)) by A52, SEQ_1:57
.= ((h ") (#) ((b ") ")) . n by SEQ_1:8
.= (((b ") (#) ((f /* (b + a)) - (f /* a))) ") . n by A47, SEQ_1:36 ; :: thesis: verum
end;
then A53: (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) = ((b ") (#) ((f /* (b + a)) - (f /* a))) " ;
diff (f,(((f | (left_open_halfline p)) ") . y0)) = diff (f,(((f | (left_open_halfline p)) ") . y0)) ;
then A54: (b ") (#) ((f /* (b + a)) - (f /* a)) is convergent by A42, A31, A35, Th12;
A55: lim ((b ") (#) ((f /* (b + a)) - (f /* a))) = diff (f,(((f | (left_open_halfline p)) ") . y0)) by A42, A31, A35, Th12;
hence (h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c)) is convergent by A53, A48, A54, A37, SEQ_2:21; :: thesis: lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0)))
thus lim ((h ") (#) ((((f | (left_open_halfline p)) ") /* (h + c)) - (((f | (left_open_halfline p)) ") /* c))) = (diff (f,(((f | (left_open_halfline p)) ") . y0))) " by A53, A48, A54, A55, A37, SEQ_2:22
.= 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) by XCMPLX_1:215 ; :: thesis: verum
end;
ex N being Neighbourhood of y0 st N c= dom ((f | (left_open_halfline p)) ") by A3, A4, A7, RCOMP_1:18;
hence ( (f | (left_open_halfline p)) " is_differentiable_in y0 & diff (((f | (left_open_halfline p)) "),y0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . y0))) ) by A10, Th12; :: thesis: verum
end;
then for y0 being Real st y0 in dom ((f | (left_open_halfline p)) ") holds
(f | (left_open_halfline p)) " is_differentiable_in y0 ;
hence (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) ") by A3, A4, FDIFF_1:9; :: thesis: for x0 being Real st x0 in dom ((f | (left_open_halfline p)) ") holds
diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0)))
let x0 be Real; :: thesis: ( x0 in dom ((f | (left_open_halfline p)) ") implies diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) )
assume x0 in dom ((f | (left_open_halfline p)) ") ; :: thesis: diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0)))
hence diff (((f | (left_open_halfline p)) "),x0) = 1 / (diff (f,(((f | (left_open_halfline p)) ") . x0))) by A6; :: thesis: verum