:: FDIFF_3 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: FDIFF_3:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th2: :: FDIFF_3:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th3: :: FDIFF_3:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: FDIFF_3:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def1 defines is_Lcontinuous_in FDIFF_3:def 1 :
:: deftheorem Def2 defines is_Rcontinuous_in FDIFF_3:def 2 :
:: deftheorem Def3 defines is_right_differentiable_in FDIFF_3:def 3 :
:: deftheorem Def4 defines is_left_differentiable_in FDIFF_3:def 4 :
theorem Th5: :: FDIFF_3:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th6: :: FDIFF_3:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: FDIFF_3:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: FDIFF_3:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :
:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :
theorem Th9: :: FDIFF_3:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm1:
for f1, f2 being PartFunc of REAL , REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ) ) holds
( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
theorem :: FDIFF_3:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm2:
for f being PartFunc of REAL , REAL
for x0 being Real st f is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0 ) ) holds
( f ^ is_left_differentiable_in x0 & Ldiff (f ^ ),x0 = - ((Ldiff f,x0) / ((f . x0) ^2 )) )
theorem :: FDIFF_3:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: FDIFF_3:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm3:
for f1, f2 being PartFunc of REAL , REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r0).] holds
f2 . g <> 0 ) ) holds
( f1 / f2 is_right_differentiable_in x0 & Rdiff (f1 / f2),x0 = (((Rdiff f1,x0) * (f2 . x0)) - ((Rdiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
theorem :: FDIFF_3:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm4:
for f being PartFunc of REAL , REAL
for x0 being Real st f is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ) ) holds
( f ^ is_right_differentiable_in x0 & Rdiff (f ^ ),x0 = - ((Rdiff f,x0) / ((f . x0) ^2 )) )
theorem :: FDIFF_3:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FDIFF_3:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)