:: ROLLE semantic presentation

theorem Th1: :: ROLLE:1
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,b2.] & b3 . b1 = b3 . b2 & b3 is_differentiable_on ].b1,b2.[ holds
ex b4 being Real st
( b4 in ].b1,b2.[ & diff b3,b4 = 0 )
proof end;

theorem Th2: :: ROLLE:2
for b1, b2 being Real st 0 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,(b1 + b2).] & b3 . b1 = b3 . (b1 + b2) & b3 is_differentiable_on ].b1,(b1 + b2).[ holds
ex b4 being Real st
( 0 < b4 & b4 < 1 & diff b3,(b1 + (b4 * b2)) = 0 )
proof end;

theorem Th3: :: ROLLE:3
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,b2.] & b3 is_differentiable_on ].b1,b2.[ holds
ex b4 being Real st
( b4 in ].b1,b2.[ & diff b3,b4 = ((b3 . b2) - (b3 . b1)) / (b2 - b1) )
proof end;

theorem Th4: :: ROLLE:4
for b1, b2 being Real st 0 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,(b1 + b2).] & b3 is_differentiable_on ].b1,(b1 + b2).[ holds
ex b4 being Real st
( 0 < b4 & b4 < 1 & b3 . (b1 + b2) = (b3 . b1) + (b2 * (diff b3,(b1 + (b4 * b2)))) )
proof end;

theorem Th5: :: ROLLE:5
for b1, b2 being Real st b1 < b2 holds
for b3, b4 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,b2.] & b3 is_differentiable_on ].b1,b2.[ & b4 is_continuous_on [.b1,b2.] & b4 is_differentiable_on ].b1,b2.[ holds
ex b5 being Real st
( b5 in ].b1,b2.[ & ((b3 . b2) - (b3 . b1)) * (diff b4,b5) = ((b4 . b2) - (b4 . b1)) * (diff b3,b5) )
proof end;

theorem Th6: :: ROLLE:6
for b1, b2 being Real st 0 < b2 holds
for b3, b4 being PartFunc of REAL , REAL st b3 is_continuous_on [.b1,(b1 + b2).] & b3 is_differentiable_on ].b1,(b1 + b2).[ & b4 is_continuous_on [.b1,(b1 + b2).] & b4 is_differentiable_on ].b1,(b1 + b2).[ & ( for b5 being Real st b5 in ].b1,(b1 + b2).[ holds
diff b4,b5 <> 0 ) holds
ex b5 being Real st
( 0 < b5 & b5 < 1 & ((b3 . (b1 + b2)) - (b3 . b1)) / ((b4 . (b1 + b2)) - (b4 . b1)) = (diff b3,(b1 + (b5 * b2))) / (diff b4,(b1 + (b5 * b2))) )
proof end;

theorem Th7: :: ROLLE:7
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
diff b3,b4 = 0 ) holds
b3 is_constant_on ].b1,b2.[
proof end;

theorem Th8: :: ROLLE:8
for b1, b2 being Real st b1 < b2 holds
for b3, b4 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & b4 is_differentiable_on ].b1,b2.[ & ( for b5 being Real st b5 in ].b1,b2.[ holds
diff b3,b5 = diff b4,b5 ) holds
( b3 - b4 is_constant_on ].b1,b2.[ & ex b5 being Real st
for b6 being Real st b6 in ].b1,b2.[ holds
b3 . b6 = (b4 . b6) + b5 )
proof end;

theorem Th9: :: ROLLE:9
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
0 < diff b3,b4 ) holds
b3 is_increasing_on ].b1,b2.[
proof end;

theorem Th10: :: ROLLE:10
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
diff b3,b4 < 0 ) holds
b3 is_decreasing_on ].b1,b2.[
proof end;

theorem Th11: :: ROLLE:11
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
0 <= diff b3,b4 ) holds
b3 is_non_decreasing_on ].b1,b2.[
proof end;

theorem Th12: :: ROLLE:12
for b1, b2 being Real st b1 < b2 holds
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
diff b3,b4 <= 0 ) holds
b3 is_non_increasing_on ].b1,b2.[
proof end;