:: ROLLE semantic presentation

theorem Th1: :: ROLLE:1

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_continuous_on [.p,g.] & f . p = f . g & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff f,x0 = 0 )

proof end;

theorem :: ROLLE:2

for x, t being Real st 0 < t holds
for f being PartFunc of REAL , REAL st f is_continuous_on [.x,(x + t).] & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & diff f,(x + (s * t)) = 0 )

proof end;

theorem Th3: :: ROLLE:3

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_continuous_on [.p,g.] & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff f,x0 = ((f . g) - (f . p)) / (g - p) )

proof end;

theorem :: ROLLE:4

for x, t being Real st 0 < t holds
for f being PartFunc of REAL , REAL st f is_continuous_on [.x,(x + t).] & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff f,(x + (s * t)))) )

proof end;

theorem Th5: :: ROLLE:5

for p, g being Real st p < g holds
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on [.p,g.] & f1 is_differentiable_on ].p,g.[ & f2 is_continuous_on [.p,g.] & 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) )

proof end;

theorem :: ROLLE:6

for x, t being Real st 0 < t holds
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on [.x,(x + t).] & f1 is_differentiable_on ].x,(x + t).[ & f2 is_continuous_on [.x,(x + t).] & 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))) )

proof end;

theorem Th7: :: ROLLE:7

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f,x = 0 ) holds
f is_constant_on ].p,g.[

proof end;

theorem :: ROLLE:8

for p, g being Real st p < g holds
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 is_constant_on ].p,g.[ & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )

proof end;

theorem :: ROLLE:9

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 < diff f,x ) holds
f is_increasing_on ].p,g.[

proof end;

theorem :: ROLLE:10

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f,x < 0 ) holds
f is_decreasing_on ].p,g.[

proof end;

theorem :: ROLLE:11

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 <= diff f,x ) holds
f is_non_decreasing_on ].p,g.[

proof end;

theorem :: ROLLE:12

for p, g being Real st p < g holds
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f,x <= 0 ) holds
f is_non_increasing_on ].p,g.[

proof end;