let p be Real; :: thesis: for f being one-to-one PartFunc of REAL ,REAL st right_open_halfline p c= dom f & f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in right_open_halfline p holds
diff f,x0 < 0 ) holds
( f | (right_open_halfline p) is one-to-one & (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) ) )
let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( right_open_halfline p c= dom f & f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in right_open_halfline p holds
diff f,x0 < 0 ) implies ( f | (right_open_halfline p) is one-to-one & (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) ) ) )
set l = right_open_halfline p;
assume that
A1: right_open_halfline p c= dom f and
A2: f is_differentiable_on right_open_halfline p and
A3: ( for x0 being Real st x0 in right_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in right_open_halfline p holds
diff f,x0 < 0 ) ; :: thesis: ( f | (right_open_halfline p) is one-to-one & (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) ) )
A4: rng (f | (right_open_halfline p)) is open by A1, A2, A3, Th43;
set f1 = f | (right_open_halfline p);
thus f | (right_open_halfline p) is one-to-one ; :: thesis: ( (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) ) )
A5: dom ((f | (right_open_halfline p)) " ) = rng (f | (right_open_halfline p)) by FUNCT_1:55;
A6: rng ((f | (right_open_halfline p)) " ) = dom (f | (right_open_halfline p)) by FUNCT_1:55;
A7: for y0 being Real st y0 in dom ((f | (right_open_halfline p)) " ) holds
( (f | (right_open_halfline p)) " is_differentiable_in y0 & diff ((f | (right_open_halfline p)) " ),y0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) )
proof
let y0 be Real; :: thesis: ( y0 in dom ((f | (right_open_halfline p)) " ) implies ( (f | (right_open_halfline p)) " is_differentiable_in y0 & diff ((f | (right_open_halfline p)) " ),y0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) ) )
assume A8: y0 in dom ((f | (right_open_halfline p)) " ) ; :: thesis: ( (f | (right_open_halfline p)) " is_differentiable_in y0 & diff ((f | (right_open_halfline p)) " ),y0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) )
then consider x0 being Real such that
A9: x0 in dom (f | (right_open_halfline p)) and
A10: y0 = (f | (right_open_halfline p)) . x0 by A5, PARTFUN1:26;
A11: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {y0} & rng (h + c) c= dom ((f | (right_open_halfline p)) " ) holds
( (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) is convergent & lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) )
proof
A12: right_open_halfline p c= dom f by A2, FDIFF_1:def 7;
( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) by A1, A2, A3, Th33, Th34;
then ((f | (right_open_halfline p)) " ) | (f .: (right_open_halfline p)) is continuous by A12, FCONT_3:27;
then A13: ((f | (right_open_halfline p)) " ) | (rng (f | (right_open_halfline p))) is continuous by RELAT_1:148;
y0 in dom (((f | (right_open_halfline p)) " ) | (rng (f | (right_open_halfline p)))) by A5, A8, RELAT_1:98;
then ((f | (right_open_halfline p)) " ) | (rng (f | (right_open_halfline p))) is_continuous_in y0 by A13, FCONT_1:def 2;
then A14: (f | (right_open_halfline p)) " is_continuous_in y0 by A5, RELAT_1:97;
reconsider a = NAT --> (((f | (right_open_halfline p)) " ) . y0) as Real_Sequence by FUNCOP_1:57;
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {y0} & rng (h + c) c= dom ((f | (right_open_halfline p)) " ) holds
( (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) is convergent & lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) )
let c be V8() Real_Sequence; :: thesis: ( rng c = {y0} & rng (h + c) c= dom ((f | (right_open_halfline p)) " ) implies ( (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) is convergent & lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) ) )
assume that
A15: rng c = {y0} and
A16: rng (h + c) c= dom ((f | (right_open_halfline p)) " ) ; :: thesis: ( (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) is convergent & lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) )
A17: lim (h + c) = y0 by A15, Th4;
reconsider a = a as V8() Real_Sequence ;
defpred S1[ Element of NAT , real number ] means for r1, r2 being real number st r1 = (h + c) . $1 & r2 = a . $1 holds
( r1 = f . (r2 + $2) & r2 + $2 in dom f & r2 + $2 in dom (f | (right_open_halfline p)) );
A18: for n being Element of NAT ex r being Real st S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Real st S1[n,r]
(h + c) . n in rng (h + c) by VALUED_0:28;
then consider g being Real such that
A19: g in dom (f | (right_open_halfline p)) and
A20: (h + c) . n = (f | (right_open_halfline p)) . g by A5, A16, PARTFUN1:26;
take r = g - x0; :: thesis: S1[n,r]
let r1, r2 be real number ; :: thesis: ( r1 = (h + c) . n & r2 = a . n implies ( r1 = f . (r2 + r) & r2 + r in dom f & r2 + r in dom (f | (right_open_halfline p)) ) )
assume that
A21: r1 = (h + c) . n and
A22: r2 = a . n ; :: thesis: ( r1 = f . (r2 + r) & r2 + r in dom f & r2 + r in dom (f | (right_open_halfline p)) )
A23: a . n = ((f | (right_open_halfline p)) " ) . ((f | (right_open_halfline p)) . x0) by A10, FUNCOP_1:13
.= x0 by A9, FUNCT_1:56 ;
hence r1 = f . (r2 + r) by A19, A20, A21, A22, FUNCT_1:70; :: thesis: ( r2 + r in dom f & r2 + r in dom (f | (right_open_halfline p)) )
g in (dom f) /\ (right_open_halfline p) by A19, RELAT_1:90;
hence ( r2 + r in dom f & r2 + r in dom (f | (right_open_halfline p)) ) by A19, A23, A22, XBOOLE_0:def 4; :: thesis: verum
end;
consider b being Real_Sequence such that
A24: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch 3(A18);
A25: now
let n be Element of NAT ; :: thesis: ((((f | (right_open_halfline p)) " ) /* (h + c)) - a) . n = b . n
A26: (h + c) . n = (h + c) . n ;
then A27: (a . n) + (b . n) in dom (f | (right_open_halfline p)) by A24;
thus ((((f | (right_open_halfline p)) " ) /* (h + c)) - a) . n = ((((f | (right_open_halfline p)) " ) /* (h + c)) . n) - (a . n) by RFUNCT_2:6
.= (((f | (right_open_halfline p)) " ) . ((h + c) . n)) - (a . n) by A16, FUNCT_2:185
.= (((f | (right_open_halfline p)) " ) . (f . ((a . n) + (b . n)))) - (a . n) by A24
.= (((f | (right_open_halfline p)) " ) . ((f | (right_open_halfline p)) . ((a . n) + (b . n)))) - (a . n) by A24, A26, FUNCT_1:70
.= ((a . n) + (b . n)) - (a . n) by A27, FUNCT_1:56
.= b . n ; :: thesis: verum
end;
A28: h + c is convergent by A15, Th4;
then A29: ((f | (right_open_halfline p)) " ) /* (h + c) is convergent by A16, A17, A14, FCONT_1:def 1;
then (((f | (right_open_halfline p)) " ) /* (h + c)) - a is convergent by SEQ_2:25;
then A30: b is convergent by A25, FUNCT_2:113;
A31: lim a = a . 0 by SEQ_4:41
.= ((f | (right_open_halfline p)) " ) . y0 by FUNCOP_1:13 ;
((f | (right_open_halfline p)) " ) . y0 = lim (((f | (right_open_halfline p)) " ) /* (h + c)) by A16, A28, A17, A14, FCONT_1:def 1;
then lim ((((f | (right_open_halfline p)) " ) /* (h + c)) - a) = (((f | (right_open_halfline p)) " ) . y0) - (((f | (right_open_halfline p)) " ) . y0) by A29, A31, SEQ_2:26
.= 0 ;
then A32: lim b = 0 by A25, FUNCT_2:113;
A33: rng (b + a) c= dom f
proof
let x be set ; :: 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
A34: x = (b + a) . n by FUNCT_2:190;
A35: (h + c) . n = (h + c) . n ;
x = (a . n) + (b . n) by A34, SEQ_1:11;
hence x in dom f by A24, A35; :: thesis: verum
end;
((f | (right_open_halfline p)) " ) . y0 in dom (f | (right_open_halfline p)) by A6, A8, FUNCT_1:def 5;
then ((f | (right_open_halfline p)) " ) . y0 in (dom f) /\ (right_open_halfline p) by RELAT_1:90;
then A36: ((f | (right_open_halfline p)) " ) . y0 in right_open_halfline p by XBOOLE_0:def 4;
then A37: f is_differentiable_in ((f | (right_open_halfline p)) " ) . y0 by A2, FDIFF_1:16;
A38: now
let n be Element of NAT ; :: thesis: c . n = (f | (right_open_halfline p)) . x0
c . n in rng c by VALUED_0:28;
hence c . n = (f | (right_open_halfline p)) . x0 by A10, A15, TARSKI:def 1; :: thesis: verum
end;
A39: 0 <> diff f,(((f | (right_open_halfline p)) " ) . y0) by A3, A36;
A40: h is non-empty by FDIFF_1:def 1;
now
given n being Element of NAT such that A41: b . n = 0 ; :: thesis: contradiction
a . n = ((f | (right_open_halfline p)) " ) . ((f | (right_open_halfline p)) . x0) by A10, FUNCOP_1:13
.= x0 by A9, FUNCT_1:56 ;
then A42: f . ((a . n) + (b . n)) = (f | (right_open_halfline p)) . x0 by A9, A41, FUNCT_1:70;
(h + c) . n = (h . n) + (c . n) by SEQ_1:11
.= (h . n) + ((f | (right_open_halfline p)) . x0) by A38 ;
then (h . n) + ((f | (right_open_halfline p)) . x0) = (f | (right_open_halfline p)) . x0 by A24, A42;
hence contradiction by A40, SEQ_1:7; :: thesis: verum
end;
then A43: b is non-empty by SEQ_1:7;
then reconsider b = b as convergent_to_0 Real_Sequence by A30, A32, FDIFF_1:def 1;
A44: b " is non-empty by A43, SEQ_1:41;
A45: rng a = {(((f | (right_open_halfline p)) " ) . y0)}
proof
thus rng a c= {(((f | (right_open_halfline p)) " ) . y0)} :: according to XBOOLE_0:def 10 :: thesis: {(((f | (right_open_halfline p)) " ) . y0)} c= rng a
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in {(((f | (right_open_halfline p)) " ) . y0)} )
assume x in rng a ; :: thesis: x in {(((f | (right_open_halfline p)) " ) . y0)}
then ex n being Element of NAT st x = a . n by FUNCT_2:190;
then x = ((f | (right_open_halfline p)) " ) . y0 by FUNCOP_1:13;
hence x in {(((f | (right_open_halfline p)) " ) . y0)} by TARSKI:def 1; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(((f | (right_open_halfline p)) " ) . y0)} or x in rng a )
assume x in {(((f | (right_open_halfline p)) " ) . y0)} ; :: thesis: x in rng a
then x = ((f | (right_open_halfline p)) " ) . y0 by TARSKI:def 1;
then a . 0 = x by FUNCOP_1:13;
hence x in rng a by VALUED_0:28; :: thesis: verum
end;
A46: rng a c= dom f
proof
let x be set ; :: 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 | (right_open_halfline p)) " ) . y0 by A45, TARSKI:def 1;
then x = x0 by A9, A10, FUNCT_1:56;
then x in (dom f) /\ (right_open_halfline p) by A9, RELAT_1:90;
hence x in dom f by XBOOLE_0:def 4; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: (f /* a) . n = c . n
A47: ((f | (right_open_halfline p)) " ) . y0 in rng ((f | (right_open_halfline p)) " ) by A8, FUNCT_1:def 5;
c . n in rng c by VALUED_0:28;
then A48: c . n = y0 by A15, TARSKI:def 1;
thus (f /* a) . n = f . (a . n) by A46, FUNCT_2:185
.= f . (((f | (right_open_halfline p)) " ) . y0) by FUNCOP_1:13
.= (f | (right_open_halfline p)) . (((f | (right_open_halfline p)) " ) . y0) by A6, A47, FUNCT_1:70
.= c . n by A5, A8, A48, FUNCT_1:57 ; :: thesis: verum
end;
then A49: f /* a = c by FUNCT_2:113;
now
let n be Element of NAT ; :: thesis: h . n = ((f /* (b + a)) - (f /* a)) . n
(h + c) . n = f . ((a . n) + (b . n)) by A24;
then (h . n) + (c . n) = f . ((a . n) + (b . n)) by SEQ_1:11;
hence h . n = (f . ((b . n) + (a . n))) - ((f /* a) . n) by A49
.= (f . ((b + a) . n)) - ((f /* a) . n) by SEQ_1:11
.= ((f /* (b + a)) . n) - ((f /* a) . n) by A33, FUNCT_2:185
.= ((f /* (b + a)) - (f /* a)) . n by RFUNCT_2:6 ;
:: thesis: verum
end;
then A50: h = (f /* (b + a)) - (f /* a) by FUNCT_2:113;
then (f /* (b + a)) - (f /* a) is non-empty by FDIFF_1:def 1;
then A51: (b " ) (#) ((f /* (b + a)) - (f /* a)) is non-empty by A44, SEQ_1:43;
A52: rng c c= dom ((f | (right_open_halfline p)) " )
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom ((f | (right_open_halfline p)) " ) )
assume x in rng c ; :: thesis: x in dom ((f | (right_open_halfline p)) " )
hence x in dom ((f | (right_open_halfline p)) " ) by A8, A15, TARSKI:def 1; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) . n = (((b " ) (#) ((f /* (b + a)) - (f /* a))) " ) . n
A53: (h + c) . n = (h + c) . n ;
then A54: (a . n) + (b . n) in dom (f | (right_open_halfline p)) by A24;
c . n in rng c by VALUED_0:28;
then A55: c . n = y0 by A15, TARSKI:def 1;
thus ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) . n = ((h " ) . n) * (((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) . n) by SEQ_1:12
.= ((h " ) . n) * (((((f | (right_open_halfline p)) " ) /* (h + c)) . n) - ((((f | (right_open_halfline p)) " ) /* c) . n)) by RFUNCT_2:6
.= ((h " ) . n) * ((((f | (right_open_halfline p)) " ) . ((h + c) . n)) - ((((f | (right_open_halfline p)) " ) /* c) . n)) by A16, FUNCT_2:185
.= ((h " ) . n) * ((((f | (right_open_halfline p)) " ) . (f . ((a . n) + (b . n)))) - ((((f | (right_open_halfline p)) " ) /* c) . n)) by A24
.= ((h " ) . n) * ((((f | (right_open_halfline p)) " ) . ((f | (right_open_halfline p)) . ((a . n) + (b . n)))) - ((((f | (right_open_halfline p)) " ) /* c) . n)) by A24, A53, FUNCT_1:70
.= ((h " ) . n) * (((a . n) + (b . n)) - ((((f | (right_open_halfline p)) " ) /* c) . n)) by A54, FUNCT_1:56
.= ((h " ) . n) * (((a . n) + (b . n)) - (((f | (right_open_halfline p)) " ) . (c . n))) by A52, FUNCT_2:185
.= ((h " ) . n) * (((a . n) + (b . n)) - (a . n)) by A55, FUNCOP_1:13
.= ((h " ) (#) ((b " ) " )) . n by SEQ_1:12
.= (((b " ) (#) ((f /* (b + a)) - (f /* a))) " ) . n by A50, SEQ_1:44 ; :: thesis: verum
end;
then A56: (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) = ((b " ) (#) ((f /* (b + a)) - (f /* a))) " by FUNCT_2:113;
diff f,(((f | (right_open_halfline p)) " ) . y0) = diff f,(((f | (right_open_halfline p)) " ) . y0) ;
then A57: (b " ) (#) ((f /* (b + a)) - (f /* a)) is convergent by A45, A33, A37, Th12;
A58: lim ((b " ) (#) ((f /* (b + a)) - (f /* a))) = diff f,(((f | (right_open_halfline p)) " ) . y0) by A45, A33, A37, Th12;
hence (h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c)) is convergent by A56, A51, A57, A39, SEQ_2:35; :: thesis: lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0))
thus lim ((h " ) (#) ((((f | (right_open_halfline p)) " ) /* (h + c)) - (((f | (right_open_halfline p)) " ) /* c))) = (diff f,(((f | (right_open_halfline p)) " ) . y0)) " by A56, A51, A57, A58, A39, SEQ_2:36
.= 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) by XCMPLX_1:217 ; :: thesis: verum
end;
ex N being Neighbourhood of y0 st N c= dom ((f | (right_open_halfline p)) " ) by A4, A5, A8, RCOMP_1:39;
hence ( (f | (right_open_halfline p)) " is_differentiable_in y0 & diff ((f | (right_open_halfline p)) " ),y0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . y0)) ) by A11, Th12; :: thesis: verum
end;
then for y0 being Real st y0 in dom ((f | (right_open_halfline p)) " ) holds
(f | (right_open_halfline p)) " is_differentiable_in y0 ;
hence (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) by A4, A5, FDIFF_1:16; :: thesis: for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0))
let x0 be Real; :: thesis: ( x0 in dom ((f | (right_open_halfline p)) " ) implies diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) )
assume x0 in dom ((f | (right_open_halfline p)) " ) ; :: thesis: diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0))
hence diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) by A7; :: thesis: verum