environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, ARYTM_3, XXREAL_1, TARSKI, RELAT_1, ORDINAL2, FUNCT_1, FDIFF_1, CARD_1, RCOMP_1, XXREAL_2, SEQ_4, XXREAL_0, XBOOLE_0, ARYTM_1, VALUED_0, SEQ_2, VALUED_1, FUNCT_2, FUNCOP_1, FUNCT_7, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, XXREAL_2, XCMPLX_0, REAL_1, RELSET_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, FDIFF_1;
definitions TARSKI;
theorems TARSKI, NAT_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1, FCONT_1, FDIFF_1, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, XXREAL_1, FUNCT_2, VALUED_0, ORDINAL1;
schemes SEQ_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, FDIFF_1, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, VALUED_1, XXREAL_2, COMPLEX1, RELSET_1, BINOP_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0;
expansions TARSKI;
theorem Th5:
for
p,
g being
Real st
p < g holds
for
f1,
f2 being
PartFunc of
REAL,
REAL st
[.p,g.] c= dom f1 &
[.p,g.] c= dom f2 &
f1 | [.p,g.] is
continuous &
f1 is_differentiable_on ].p,g.[ &
f2 | [.p,g.] is
continuous &
f2 is_differentiable_on ].p,g.[ holds
ex
x0 being
Real st
(
x0 in ].p,g.[ &
((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
theorem
for
x,
t being
Real st
0 < t holds
for
f1,
f2 being
PartFunc of
REAL,
REAL st
[.x,(x + t).] c= dom f1 &
[.x,(x + t).] c= dom f2 &
f1 | [.x,(x + t).] is
continuous &
f1 is_differentiable_on ].x,(x + t).[ &
f2 | [.x,(x + t).] is
continuous &
f2 is_differentiable_on ].x,(x + t).[ & ( for
x1 being
Real st
x1 in ].x,(x + t).[ holds
diff (
f2,
x1)
<> 0 ) holds
ex
s being
Real st
(
0 < s &
s < 1 &
((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
theorem
for
p,
g being
Real for
f1,
f2 being
PartFunc of
REAL,
REAL st
f1 is_differentiable_on ].p,g.[ &
f2 is_differentiable_on ].p,g.[ & ( for
x being
Real st
x in ].p,g.[ holds
diff (
f1,
x)
= diff (
f2,
x) ) holds
(
(f1 - f2) | ].p,g.[ is
V8() & ex
r being
Real st
for
x being
Real st
x in ].p,g.[ holds
f1 . x = (f2 . x) + r )