:: DIFF_2 semantic presentation begin theorem Th1: :: DIFF_2:1 for x, h being Real for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h proof let x, h be Real; ::_thesis: for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h let f be Function of REAL,REAL; ::_thesis: [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h [!f,x,(x + h)!] = [!f,(x + h),x!] by DIFF_1:29 .= ((fD (f,h)) . x) / h by DIFF_1:3 .= ((fD (((fdif (f,h)) . 0),h)) . x) / h by DIFF_1:def_6 .= (((fdif (f,h)) . (0 + 1)) . x) / h by DIFF_1:def_6 ; hence [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h ; ::_thesis: verum end; theorem :: DIFF_2:2 for h, x being Real for f being Function of REAL,REAL st h <> 0 holds [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL st h <> 0 holds [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) let f be Function of REAL,REAL; ::_thesis: ( h <> 0 implies [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ) A1: (fdif (f,h)) . 1 is Function of REAL,REAL by DIFF_1:2; assume A2: h <> 0 ; ::_thesis: [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) then A3: x + h <> x + (2 * h) ; ( x <> x + h & x <> x + (2 * h) ) by A2; then x,x + h,x + (2 * h) are_mutually_different by A3, ZFMISC_1:def_5; then [!f,x,(x + h),(x + (2 * h))!] = [!f,(x + (2 * h)),(x + h),x!] by DIFF_1:34 .= ([!f,(x + h),(x + (2 * h))!] - [!f,(x + h),x!]) / ((x + (2 * h)) - x) by DIFF_1:29 .= ([!f,(x + h),((x + h) + h)!] - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by DIFF_1:29 .= (((((fdif (f,h)) . 1) . (x + h)) / h) - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by Th1 .= (((((fdif (f,h)) . 1) . (x + h)) / h) - ((((fdif (f,h)) . 1) . x) / h)) / ((x + (2 * h)) - x) by Th1 .= (((((fdif (f,h)) . 1) . (x + h)) - (((fdif (f,h)) . 1) . x)) / h) / ((x + (2 * h)) - x) by XCMPLX_1:120 .= (((fD (((fdif (f,h)) . 1),h)) . x) / h) / (2 * h) by A1, DIFF_1:3 .= ((((fdif (f,h)) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def_6 .= (((fdif (f,h)) . 2) . x) / (h * (2 * h)) by XCMPLX_1:78 .= (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ; hence [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ; ::_thesis: verum end; theorem Th3: :: DIFF_2:3 for x, h being Real for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h proof let x, h be Real; ::_thesis: for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h let f be Function of REAL,REAL; ::_thesis: [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h [!f,(x - h),x!] = [!f,x,(x - h)!] by DIFF_1:29 .= ((bD (f,h)) . x) / h by DIFF_1:4 .= ((bD (((bdif (f,h)) . 0),h)) . x) / h by DIFF_1:def_7 .= (((bdif (f,h)) . (0 + 1)) . x) / h by DIFF_1:def_7 ; hence [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h ; ::_thesis: verum end; theorem :: DIFF_2:4 for h, x being Real for f being Function of REAL,REAL st h <> 0 holds [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL st h <> 0 holds [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) let f be Function of REAL,REAL; ::_thesis: ( h <> 0 implies [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) ) set y = x - h; A1: (bdif (f,h)) . 1 is Function of REAL,REAL by DIFF_1:12; assume A2: h <> 0 ; ::_thesis: [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) then A3: x - h <> x - (2 * h) ; ( x <> x - h & x <> x - (2 * h) ) by A2; then x,x - h,x - (2 * h) are_mutually_different by A3, ZFMISC_1:def_5; then [!f,(x - (2 * h)),(x - h),x!] = [!f,x,(x - h),(x - (2 * h))!] by DIFF_1:34 .= ([!f,(x - h),x!] - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by DIFF_1:29 .= (((((bdif (f,h)) . 1) . x) / h) - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by Th3 .= (((((bdif (f,h)) . 1) . x) / h) - [!f,((x - h) - h),(x - h)!]) / (x - (x - (2 * h))) by DIFF_1:29 .= (((((bdif (f,h)) . 1) . x) / h) - ((((bdif (f,h)) . 1) . (x - h)) / h)) / (x - (x - (2 * h))) by Th3 .= (((((bdif (f,h)) . 1) . x) - (((bdif (f,h)) . 1) . (x - h))) / h) / (x - (x - (2 * h))) by XCMPLX_1:120 .= (((bD (((bdif (f,h)) . 1),h)) . x) / h) / (2 * h) by A1, DIFF_1:4 .= ((((bdif (f,h)) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def_7 .= (((bdif (f,h)) . 2) . x) / (h * (2 * h)) by XCMPLX_1:78 .= (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) ; hence [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) ; ::_thesis: verum end; theorem Th5: :: DIFF_2:5 for r, x0, x1, x2 being Real for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!] proof let r, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!] let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!] [!(r (#) f),x0,x1,x2!] = ((r * [!f,x0,x1!]) - [!(r (#) f),x1,x2!]) / (x0 - x2) by DIFF_1:31 .= ((r * [!f,x0,x1!]) - (r * [!f,x1,x2!])) / (x0 - x2) by DIFF_1:31 .= (r * ([!f,x0,x1!] - [!f,x1,x2!])) / (x0 - x2) ; hence [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!] by XCMPLX_1:74; ::_thesis: verum end; theorem Th6: :: DIFF_2:6 for x0, x1, x2 being Real for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!] proof let x0, x1, x2 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!] let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!] [!(f1 + f2),x0,x1,x2!] = (([!f1,x0,x1!] + [!f2,x0,x1!]) - [!(f1 + f2),x1,x2!]) / (x0 - x2) by DIFF_1:32 .= (([!f1,x0,x1!] + [!f2,x0,x1!]) - ([!f1,x1,x2!] + [!f2,x1,x2!])) / (x0 - x2) by DIFF_1:32 .= (([!f1,x0,x1!] - [!f1,x1,x2!]) + ([!f2,x0,x1!] - [!f2,x1,x2!])) / (x0 - x2) ; hence [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!] by XCMPLX_1:62; ::_thesis: verum end; theorem :: DIFF_2:7 for r1, r2, x0, x1, x2 being Real for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!]) proof let r1, r2, x0, x1, x2 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!]) let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!]) [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = [!(r1 (#) f1),x0,x1,x2!] + [!(r2 (#) f2),x0,x1,x2!] by Th6 .= (r1 * [!f1,x0,x1,x2!]) + [!(r2 (#) f2),x0,x1,x2!] by Th5 ; hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!]) by Th5; ::_thesis: verum end; theorem Th8: :: DIFF_2:8 for r, x0, x1, x2, x3 being Real for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!] proof let r, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!] let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!] [!(r (#) f),x0,x1,x2,x3!] = ((r * [!f,x0,x1,x2!]) - [!(r (#) f),x1,x2,x3!]) / (x0 - x3) by Th5 .= ((r * [!f,x0,x1,x2!]) - (r * [!f,x1,x2,x3!])) / (x0 - x3) by Th5 .= (r * ([!f,x0,x1,x2!] - [!f,x1,x2,x3!])) / (x0 - x3) ; hence [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!] by XCMPLX_1:74; ::_thesis: verum end; theorem Th9: :: DIFF_2:9 for x0, x1, x2, x3 being Real for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!] proof let x0, x1, x2, x3 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!] let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!] [!(f1 + f2),x0,x1,x2,x3!] = (([!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]) - [!(f1 + f2),x1,x2,x3!]) / (x0 - x3) by Th6 .= (([!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]) - ([!f1,x1,x2,x3!] + [!f2,x1,x2,x3!])) / (x0 - x3) by Th6 .= (([!f1,x0,x1,x2!] - [!f1,x1,x2,x3!]) + ([!f2,x0,x1,x2!] - [!f2,x1,x2,x3!])) / (x0 - x3) ; hence [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!] by XCMPLX_1:62; ::_thesis: verum end; theorem :: DIFF_2:10 for r1, r2, x0, x1, x2, x3 being Real for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!]) proof let r1, r2, x0, x1, x2, x3 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!]) let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!]) [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = [!(r1 (#) f1),x0,x1,x2,x3!] + [!(r2 (#) f2),x0,x1,x2,x3!] by Th9 .= (r1 * [!f1,x0,x1,x2,x3!]) + [!(r2 (#) f2),x0,x1,x2,x3!] by Th8 ; hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!]) by Th8; ::_thesis: verum end; definition let f be real-valued Function; let x0, x1, x2, x3, x4 be real number ; func[!f,x0,x1,x2,x3,x4!] -> Real equals :: DIFF_2:def 1 ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4); correctness coherence ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4) is Real; ; end; :: deftheorem defines [! DIFF_2:def_1_:_ for f being real-valued Function for x0, x1, x2, x3, x4 being real number holds [!f,x0,x1,x2,x3,x4!] = ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4); theorem Th11: :: DIFF_2:11 for r, x0, x1, x2, x3, x4 being Real for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!] proof let r, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!] let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!] [!(r (#) f),x0,x1,x2,x3,x4!] = ((r * [!f,x0,x1,x2,x3!]) - [!(r (#) f),x1,x2,x3,x4!]) / (x0 - x4) by Th8 .= ((r * [!f,x0,x1,x2,x3!]) - (r * [!f,x1,x2,x3,x4!])) / (x0 - x4) by Th8 .= (r * ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!])) / (x0 - x4) ; hence [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!] by XCMPLX_1:74; ::_thesis: verum end; theorem Th12: :: DIFF_2:12 for x0, x1, x2, x3, x4 being Real for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!] proof let x0, x1, x2, x3, x4 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!] let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!] [!(f1 + f2),x0,x1,x2,x3,x4!] = (([!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]) - [!(f1 + f2),x1,x2,x3,x4!]) / (x0 - x4) by Th9 .= (([!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]) - ([!f1,x1,x2,x3,x4!] + [!f2,x1,x2,x3,x4!])) / (x0 - x4) by Th9 .= (([!f1,x0,x1,x2,x3!] - [!f1,x1,x2,x3,x4!]) + ([!f2,x0,x1,x2,x3!] - [!f2,x1,x2,x3,x4!])) / (x0 - x4) ; hence [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!] by XCMPLX_1:62; ::_thesis: verum end; theorem :: DIFF_2:13 for r1, r2, x0, x1, x2, x3, x4 being Real for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) proof let r1, r2, x0, x1, x2, x3, x4 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = [!(r1 (#) f1),x0,x1,x2,x3,x4!] + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th12 .= (r1 * [!f1,x0,x1,x2,x3,x4!]) + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th11 ; hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) by Th11; ::_thesis: verum end; definition let f be real-valued Function; let x0, x1, x2, x3, x4, x5 be real number ; func[!f,x0,x1,x2,x3,x4,x5!] -> Real equals :: DIFF_2:def 2 ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5); correctness coherence ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5) is Real; ; end; :: deftheorem defines [! DIFF_2:def_2_:_ for f being real-valued Function for x0, x1, x2, x3, x4, x5 being real number holds [!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5); theorem Th14: :: DIFF_2:14 for r, x0, x1, x2, x3, x4, x5 being Real for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] proof let r, x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] [!(r (#) f),x0,x1,x2,x3,x4,x5!] = ((r * [!f,x0,x1,x2,x3,x4!]) - [!(r (#) f),x1,x2,x3,x4,x5!]) / (x0 - x5) by Th11 .= ((r * [!f,x0,x1,x2,x3,x4!]) - (r * [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) by Th11 .= (r * ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) ; hence [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] by XCMPLX_1:74; ::_thesis: verum end; theorem Th15: :: DIFF_2:15 for x0, x1, x2, x3, x4, x5 being Real for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!] proof let x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!] let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!] [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = (([!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]) - [!(f1 + f2),x1,x2,x3,x4,x5!]) / (x0 - x5) by Th12 .= (([!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]) - ([!f1,x1,x2,x3,x4,x5!] + [!f2,x1,x2,x3,x4,x5!])) / (x0 - x5) by Th12 .= (([!f1,x0,x1,x2,x3,x4!] - [!f1,x1,x2,x3,x4,x5!]) + ([!f2,x0,x1,x2,x3,x4!] - [!f2,x1,x2,x3,x4,x5!])) / (x0 - x5) ; hence [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!] by XCMPLX_1:62; ::_thesis: verum end; theorem :: DIFF_2:16 for r1, r2, x0, x1, x2, x3, x4, x5 being Real for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!]) proof let r1, r2, x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!]) let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!]) [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = [!(r1 (#) f1),x0,x1,x2,x3,x4,x5!] + [!(r2 (#) f2),x0,x1,x2,x3,x4,x5!] by Th15 .= (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + [!(r2 (#) f2),x0,x1,x2,x3,x4,x5!] by Th14 ; hence [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!]) by Th14; ::_thesis: verum end; theorem :: DIFF_2:17 for x0, x1, x2 being Real for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) proof let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) ) assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) then A2: x1 - x2 <> 0 by ZFMISC_1:def_5; A3: x0 - x1 <> 0 by A1, ZFMISC_1:def_5; A4: x0 - x2 <> 0 by A1, ZFMISC_1:def_5; [!f,x0,x1,x2!] = ((((f . x0) - (f . x1)) / (x0 - x1)) / (x0 - x2)) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:120 .= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:78 .= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:78 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:120 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) / ((x1 - x2) * (x0 - x2))) - ((f . x2) / ((x1 - x2) * (x0 - x2)))) by XCMPLX_1:120 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A2, XCMPLX_1:91 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + (((f . x1) * (x0 - x1)) / (((x1 - x2) * (x0 - x2)) * (x0 - x1))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A3, XCMPLX_1:91 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) + ((f . x1) * (x0 - x1))) / (((x0 - x1) * (x0 - x2)) * (x1 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:62 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) * (x0 - x2)) / (((x0 - x1) * (x1 - x2)) * (x0 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) .= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / (- ((x1 - x0) * (x1 - x2))))) + ((f . x2) / (- ((x2 - x1) * (x0 - x2)))) by A4, XCMPLX_1:91 .= (((f . x0) / ((x0 - x1) * (x0 - x2))) + (- ((f . x1) / (- ((x1 - x0) * (x1 - x2)))))) + ((f . x2) / ((- (x2 - x1)) * (- (x2 - x0)))) ; hence [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) by XCMPLX_1:189; ::_thesis: verum end; theorem :: DIFF_2:18 for x0, x1, x2, x3 being Real for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) proof let x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) ) set x10 = x1 - x0; set x20 = x2 - x0; set x30 = x3 - x0; set x12 = x1 - x2; set x13 = x1 - x3; set x23 = x2 - x3; assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) then A2: x2 - x3 <> 0 by ZFMISC_1:def_6; A3: x3 - x0 <> 0 by A1, ZFMISC_1:def_6; A4: x1 - x3 <> 0 by A1, ZFMISC_1:def_6; A5: x1 - x0 <> 0 by A1, ZFMISC_1:def_6; A6: x2 - x0 <> 0 by A1, ZFMISC_1:def_6; A7: x1 - x2 <> 0 by A1, ZFMISC_1:def_6; A8: [!f,x0,x1,x2,x3!] = ((((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) .= ((((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:188 .= (((- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) .= ((((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:191 .= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A7, A5, XCMPLX_1:116 .= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A2, A7, XCMPLX_1:130 .= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:78 .= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3)))) / (x0 - x3) by XCMPLX_1:78 .= (- ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))))) / (- (x0 - x3)) by XCMPLX_1:191 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0) .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x3 - x0)) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:120 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:78 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x2 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0)) * (x2 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A6, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0))) * (x1 - x0)) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A5, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) * ((x2 - x3) * (x1 - x3))) / (((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x1 - x0)) * ((x2 - x3) * (x1 - x3)))) by A2, A4, XCMPLX_1:6, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) * (x2 - x3)) * (x1 - x3)) + (((((f . x1) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x1 - x3)))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) by XCMPLX_1:120 .= ((((- ((((f . x0) * (x1 - x2)) * (x2 - x3)) * (x1 - x3))) + ((((f . x1) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((f . x2) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) + ((((f . x3) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) ; A9: [!f,x3,x2,x1,x0!] = ((((((f . x3) - (f . x2)) / (- (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) .= ((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188 .= ((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (- (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188 .= (((- ((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) .= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:191 .= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((- (((f . x2) - (f . x1)) / (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188 .= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (- ((- ((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2)))) / (x2 - x0)))) / (x3 - x0) .= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:190 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0) by A2, A7, XCMPLX_1:130 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0) by A7, A5, XCMPLX_1:116 .= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:78 .= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0) by XCMPLX_1:78 .= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) * (x1 - x3)) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x1 - x3)))) / (x3 - x0) by A4, XCMPLX_1:91 .= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) + ((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3))) * (x2 - x3)) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A2, XCMPLX_1:91 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) * (x2 - x0)) / ((((x2 - x3) * (x1 - x2)) * (x1 - x3)) * (x2 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A6, XCMPLX_1:91 .= ((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) - ((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0))) * (x1 - x0)) / (((((x1 - x2) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x1 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A5, XCMPLX_1:91 .= ((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) by XCMPLX_1:62 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) by XCMPLX_1:78 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) by XCMPLX_1:78 .= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3)))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) by XCMPLX_1:62 .= [!f,x0,x1,x2,x3!] by A8 ; [!f,x1,x2,x3,x0!] = (((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - (((((f . x2) - (f . x3)) / (x2 - x3)) - (((f . x3) - (f . x0)) / (x3 - x0))) / (x2 - x0))) / (x1 - x0) by A2, A7, XCMPLX_1:130 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0) by A2, A3, XCMPLX_1:130 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0)))) / (x1 - x0) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x1 - x0)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0)) by XCMPLX_1:120 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0)) by XCMPLX_1:78 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by A3, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0))) * (x2 - x0)) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by A6, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) * (x1 - x3)) / (((((x1 - x0) * (x3 - x0)) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A4, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) - ((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3))) * (x1 - x2)) / ((((((x2 - x3) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0)) * (x1 - x2))) by A7, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) * (x1 - x2)) - (((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0)) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8 ; hence ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) by A9; ::_thesis: verum end; theorem :: DIFF_2:19 for x0, x1, x2, x3 being Real for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) proof let x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) ) set x10 = x1 - x0; set x20 = x2 - x0; set x30 = x3 - x0; set x12 = x1 - x2; set x13 = x1 - x3; set x23 = x2 - x3; assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) then A2: x2 - x3 <> 0 by ZFMISC_1:def_6; A3: x1 - x3 <> 0 by A1, ZFMISC_1:def_6; A4: x1 - x2 <> 0 by A1, ZFMISC_1:def_6; A5: x3 - x0 <> 0 by A1, ZFMISC_1:def_6; A6: x2 - x0 <> 0 by A1, ZFMISC_1:def_6; A7: x1 - x0 <> 0 by A1, ZFMISC_1:def_6; A8: [!f,x0,x1,x2,x3!] = ((((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) .= ((((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:188 .= (((- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) .= ((((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:191 .= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A4, A7, XCMPLX_1:116 .= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A2, A4, XCMPLX_1:130 .= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:78 .= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3)))) / (x0 - x3) by XCMPLX_1:78 .= (- ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))))) / (- (x0 - x3)) by XCMPLX_1:191 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0) .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x3 - x0)) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:120 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:78 .= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x2 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0)) * (x2 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A6, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0))) * (x1 - x0)) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A7, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) * ((x2 - x3) * (x1 - x3))) / (((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x1 - x0)) * ((x2 - x3) * (x1 - x3)))) by A2, A3, XCMPLX_1:6, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) * (x2 - x3)) * (x1 - x3)) + (((((f . x1) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x1 - x3)))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) by XCMPLX_1:120 .= ((((- ((((f . x0) * (x1 - x2)) * (x2 - x3)) * (x1 - x3))) + ((((f . x1) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((f . x2) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) + ((((f . x3) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) ; A9: [!f,x1,x2,x0,x3!] = ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (((f . x0) - (f . x3)) / (- (x3 - x0)))) / (x2 - x3))) / (x1 - x3) .= ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (- (((f . x0) - (f . x3)) / (x3 - x0)))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:188 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) + (((f . x0) - (f . x3)) / (x3 - x0))) / (x2 - x3))) / (x1 - x3) by A4, A6, XCMPLX_1:130 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by A5, A6, XCMPLX_1:116 .= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3)))) / (x1 - x3) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) / (x1 - x3)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:120 .= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:78 .= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by XCMPLX_1:78 .= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A5, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) - ((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0))) * (x2 - x3)) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A2, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) * (x1 - x2)) / (((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2))) by A4, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) + ((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2))) * (x1 - x0)) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0))) by A7, XCMPLX_1:91 .= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) * (x1 - x0)) + (((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2)) * (x1 - x0)))) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0)) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8 ; [!f,x1,x0,x2,x3!] = ((((((f . x1) - (f . x0)) / (x1 - x0)) - (- (((f . x0) - (f . x2)) / (x2 - x0)))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (- (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x0 - x3))) / (x1 - x3) by XCMPLX_1:188 .= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((- (((f . x0) - (f . x2)) / (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (- (x3 - x0)))) / (x1 - x3) by XCMPLX_1:188 .= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - ((- ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3)))) / (- (x3 - x0)))) / (x1 - x3) .= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:191 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x2 - x0) * (x1 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by A6, A7, XCMPLX_1:116 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x2 - x0))) / (x1 - x2)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by A2, A6, XCMPLX_1:116 .= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:78 .= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0)))) / (x1 - x3) by XCMPLX_1:78 .= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) / (x1 - x3)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:120 .= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:78 .= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by XCMPLX_1:78 .= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) * (x2 - x3)) / (((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A2, XCMPLX_1:91 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) + ((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3))) * (x3 - x0)) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A5, XCMPLX_1:91 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) * (x1 - x0)) / (((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0))) by A7, XCMPLX_1:91 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) + ((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0))) * (x1 - x2)) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2))) by A4, XCMPLX_1:91 .= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) * (x1 - x2)) + (((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0)) * (x1 - x2)))) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2)) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8 ; hence ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) by A9; ::_thesis: verum end; theorem :: DIFF_2:20 for x0, x1, x2 being Real for f being Function of REAL,REAL st f is constant holds [!f,x0,x1,x2!] = 0 proof let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds [!f,x0,x1,x2!] = 0 let f be Function of REAL,REAL; ::_thesis: ( f is constant implies [!f,x0,x1,x2!] = 0 ) assume A1: f is constant ; ::_thesis: [!f,x0,x1,x2!] = 0 then [!f,x0,x1,x2!] = (0 - [!f,x1,x2!]) / (x0 - x2) by DIFF_1:30 .= (0 - 0) / (x0 - x2) by A1, DIFF_1:30 ; hence [!f,x0,x1,x2!] = 0 ; ::_thesis: verum end; theorem Th21: :: DIFF_2:21 for x0, x1, a, b being Real st x0 <> x1 holds [!(AffineMap (a,b)),x0,x1!] = a proof let x0, x1, a, b be Real; ::_thesis: ( x0 <> x1 implies [!(AffineMap (a,b)),x0,x1!] = a ) assume x0 <> x1 ; ::_thesis: [!(AffineMap (a,b)),x0,x1!] = a then A1: x0 - x1 <> 0 ; [!(AffineMap (a,b)),x0,x1!] = (((a * x0) + b) - ((AffineMap (a,b)) . x1)) / (x0 - x1) by FCONT_1:def_4 .= (((a * x0) + b) - ((a * x1) + b)) / (x0 - x1) by FCONT_1:def_4 .= (a * (x0 - x1)) / (x0 - x1) ; hence [!(AffineMap (a,b)),x0,x1!] = a by A1, XCMPLX_1:89; ::_thesis: verum end; theorem Th22: :: DIFF_2:22 for x0, x1, x2, a, b being Real st x0,x1,x2 are_mutually_different holds [!(AffineMap (a,b)),x0,x1,x2!] = 0 proof let x0, x1, x2, a, b be Real; ::_thesis: ( x0,x1,x2 are_mutually_different implies [!(AffineMap (a,b)),x0,x1,x2!] = 0 ) assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: [!(AffineMap (a,b)),x0,x1,x2!] = 0 then A2: x1 <> x2 by ZFMISC_1:def_5; x0 <> x1 by A1, ZFMISC_1:def_5; then [!(AffineMap (a,b)),x0,x1,x2!] = (a - [!(AffineMap (a,b)),x1,x2!]) / (x0 - x2) by Th21 .= (a - a) / (x0 - x2) by A2, Th21 ; hence [!(AffineMap (a,b)),x0,x1,x2!] = 0 ; ::_thesis: verum end; theorem :: DIFF_2:23 for x0, x1, x2, x3, a, b being Real st x0,x1,x2,x3 are_mutually_different holds [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 proof let x0, x1, x2, x3, a, b be Real; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 ) assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 then A2: x1 <> x2 by ZFMISC_1:def_6; ( x1 <> x3 & x2 <> x3 ) by A1, ZFMISC_1:def_6; then A3: x1,x2,x3 are_mutually_different by A2, ZFMISC_1:def_5; ( x0 <> x1 & x0 <> x2 ) by A1, ZFMISC_1:def_6; then x0,x1,x2 are_mutually_different by A2, ZFMISC_1:def_5; then [!(AffineMap (a,b)),x0,x1,x2,x3!] = (0 - [!(AffineMap (a,b)),x1,x2,x3!]) / (x0 - x3) by Th22 .= (0 - 0) / (x0 - x3) by A3, Th22 ; hence [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 ; ::_thesis: verum end; theorem :: DIFF_2:24 for a, b, h, x being Real holds (fD ((AffineMap (a,b)),h)) . x = a * h proof let a, b, h, x be Real; ::_thesis: (fD ((AffineMap (a,b)),h)) . x = a * h (fD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . (x + h)) - ((AffineMap (a,b)) . x) by DIFF_1:3 .= ((a * (x + h)) + b) - ((AffineMap (a,b)) . x) by FCONT_1:def_4 .= (((a * x) + (a * h)) + b) - ((a * x) + b) by FCONT_1:def_4 ; hence (fD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum end; theorem :: DIFF_2:25 for a, b, h, x being Real holds (bD ((AffineMap (a,b)),h)) . x = a * h proof let a, b, h, x be Real; ::_thesis: (bD ((AffineMap (a,b)),h)) . x = a * h (bD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . x) - ((AffineMap (a,b)) . (x - h)) by DIFF_1:4 .= ((a * x) + b) - ((AffineMap (a,b)) . (x - h)) by FCONT_1:def_4 .= ((a * x) + b) - ((a * (x - h)) + b) by FCONT_1:def_4 ; hence (bD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum end; theorem :: DIFF_2:26 for a, b, h, x being Real holds (cD ((AffineMap (a,b)),h)) . x = a * h proof let a, b, h, x be Real; ::_thesis: (cD ((AffineMap (a,b)),h)) . x = a * h (cD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . (x + (h / 2))) - ((AffineMap (a,b)) . (x - (h / 2))) by DIFF_1:5 .= ((a * (x + (h / 2))) + b) - ((AffineMap (a,b)) . (x - (h / 2))) by FCONT_1:def_4 .= ((a * (x + (h / 2))) + b) - ((a * (x - (h / 2))) + b) by FCONT_1:def_4 ; hence (cD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum end; theorem Th27: :: DIFF_2:27 for a, b, c, x0, x1 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 holds [!f,x0,x1!] = (a * (x0 + x1)) + b proof let a, b, c, x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 holds [!f,x0,x1!] = (a * (x0 + x1)) + b let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 implies [!f,x0,x1!] = (a * (x0 + x1)) + b ) assume that A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c and A2: x0 <> x1 ; ::_thesis: [!f,x0,x1!] = (a * (x0 + x1)) + b A3: x0 - x1 <> 0 by A2; [!f,x0,x1!] = ((((a * (x0 ^2)) + (b * x0)) + c) - (f . x1)) / (x0 - x1) by A1 .= ((((a * (x0 ^2)) + (b * x0)) + c) - (((a * (x1 ^2)) + (b * x1)) + c)) / (x0 - x1) by A1 .= (((a * (x0 + x1)) + b) * (x0 - x1)) / (x0 - x1) ; hence [!f,x0,x1!] = (a * (x0 + x1)) + b by A3, XCMPLX_1:89; ::_thesis: verum end; theorem Th28: :: DIFF_2:28 for a, b, c, x0, x1, x2 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = a proof let a, b, c, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = a let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = a ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2 are_mutually_different or [!f,x0,x1,x2!] = a ) assume A2: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = a then A3: x1 <> x2 by ZFMISC_1:def_5; A4: x0 - x2 <> 0 by A2, ZFMISC_1:def_5; x0 <> x1 by A2, ZFMISC_1:def_5; then [!f,x0,x1,x2!] = (((a * (x0 + x1)) + b) - [!f,x1,x2!]) / (x0 - x2) by A1, Th27 .= (((a * (x0 + x1)) + b) - ((a * (x1 + x2)) + b)) / (x0 - x2) by A1, A3, Th27 .= (a * (x0 - x2)) / (x0 - x2) ; hence [!f,x0,x1,x2!] = a by A4, XCMPLX_1:89; ::_thesis: verum end; theorem Th29: :: DIFF_2:29 for a, b, c, x0, x1, x2, x3 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = 0 proof let a, b, c, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = 0 let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = 0 ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2,x3 are_mutually_different or [!f,x0,x1,x2,x3!] = 0 ) assume A2: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = 0 then A3: x1 <> x2 by ZFMISC_1:def_6; ( x1 <> x3 & x2 <> x3 ) by A2, ZFMISC_1:def_6; then A4: x1,x2,x3 are_mutually_different by A3, ZFMISC_1:def_5; ( x0 <> x1 & x0 <> x2 ) by A2, ZFMISC_1:def_6; then x0,x1,x2 are_mutually_different by A3, ZFMISC_1:def_5; then [!f,x0,x1,x2,x3!] = (a - [!f,x1,x2,x3!]) / (x0 - x3) by A1, Th28 .= (a - a) / (x0 - x3) by A1, A4, Th28 ; hence [!f,x0,x1,x2,x3!] = 0 ; ::_thesis: verum end; theorem :: DIFF_2:30 for a, b, c, x0, x1, x2, x3, x4 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different holds [!f,x0,x1,x2,x3,x4!] = 0 proof let a, b, c, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different holds [!f,x0,x1,x2,x3,x4!] = 0 let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different implies [!f,x0,x1,x2,x3,x4!] = 0 ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2,x3,x4 are_mutually_different or [!f,x0,x1,x2,x3,x4!] = 0 ) assume A2: x0,x1,x2,x3,x4 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3,x4!] = 0 then A3: ( x1 <> x2 & x1 <> x3 ) by ZFMISC_1:def_7; A4: x0 <> x3 by A2, ZFMISC_1:def_7; A5: x2 <> x3 by A2, ZFMISC_1:def_7; A6: x3 <> x4 by A2, ZFMISC_1:def_7; ( x1 <> x4 & x2 <> x4 ) by A2, ZFMISC_1:def_7; then A7: x1,x2,x3,x4 are_mutually_different by A3, A5, A6, ZFMISC_1:def_6; ( x0 <> x1 & x0 <> x2 ) by A2, ZFMISC_1:def_7; then x0,x1,x2,x3 are_mutually_different by A4, A3, A5, ZFMISC_1:def_6; then [!f,x0,x1,x2,x3,x4!] = (0 - [!f,x1,x2,x3,x4!]) / (x0 - x4) by A1, Th29 .= (0 - 0) / (x0 - x4) by A1, A7, Th29 ; hence [!f,x0,x1,x2,x3,x4!] = 0 ; ::_thesis: verum end; theorem :: DIFF_2:31 for a, b, c, h being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) proof let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) let x be Real; ::_thesis: (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) (fD (f,h)) . x = (f . (x + h)) - (f . x) by DIFF_1:3 .= (((a * ((x + h) ^2)) + (b * (x + h))) + c) - (f . x) by A1 .= (((a * ((x + h) ^2)) + (b * (x + h))) + c) - (((a * (x ^2)) + (b * x)) + c) by A1 .= ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) ; hence (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) ; ::_thesis: verum end; theorem :: DIFF_2:32 for a, b, c, h being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) proof let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) let x be Real; ::_thesis: (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) (bD (f,h)) . x = (f . x) - (f . (x - h)) by DIFF_1:4 .= (((a * (x ^2)) + (b * x)) + c) - (f . (x - h)) by A1 .= (((a * (x ^2)) + (b * x)) + c) - (((a * ((x - h) ^2)) + (b * (x - h))) + c) by A1 .= ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) ; hence (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) ; ::_thesis: verum end; theorem :: DIFF_2:33 for a, b, c, h being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) proof let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) ) assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) let x be Real; ::_thesis: (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5 .= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (f . (x - (h / 2))) by A1 .= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (((a * ((x - (h / 2)) ^2)) + (b * (x - (h / 2)))) + c) by A1 .= (((2 * a) * h) * x) + (b * h) ; hence (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) ; ::_thesis: verum end; theorem Th34: :: DIFF_2:34 for k, x0, x1 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 holds [!f,x0,x1!] = - (k / (x0 * x1)) proof let k, x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 holds [!f,x0,x1!] = - (k / (x0 * x1)) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 implies [!f,x0,x1!] = - (k / (x0 * x1)) ) assume that A1: for x being Real holds f . x = k / x and A2: x0 <> x1 and A3: x0 <> 0 and A4: x1 <> 0 ; ::_thesis: [!f,x0,x1!] = - (k / (x0 * x1)) A5: x1 - x0 <> 0 by A2; [!f,x0,x1!] = ((k / x0) - (f . x1)) / (x0 - x1) by A1 .= ((k / x0) - (k / x1)) / (x0 - x1) by A1 .= (((k * x1) / (x0 * x1)) - (k / x1)) / (x0 - x1) by A4, XCMPLX_1:91 .= (((k * x1) / (x0 * x1)) - ((k * x0) / (x0 * x1))) / (x0 - x1) by A3, XCMPLX_1:91 .= (((k * x1) - (k * x0)) / (x0 * x1)) / (x0 - x1) by XCMPLX_1:120 .= ((k * (x1 - x0)) / (x0 * x1)) / (- (x1 - x0)) .= - (((k * (x1 - x0)) / (x0 * x1)) / (x1 - x0)) by XCMPLX_1:188 .= - (((k * (x1 - x0)) / (x1 - x0)) / (x0 * x1)) by XCMPLX_1:48 ; hence [!f,x0,x1!] = - (k / (x0 * x1)) by A5, XCMPLX_1:89; ::_thesis: verum end; theorem Th35: :: DIFF_2:35 for k, x0, x1, x2 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) proof let k, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different holds [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) ) assume that A1: for x being Real holds f . x = k / x and A2: x0 <> 0 and A3: x1 <> 0 and A4: x2 <> 0 ; ::_thesis: ( not x0,x1,x2 are_mutually_different or [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) ) assume A5: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) then A6: x1 <> x2 by ZFMISC_1:def_5; A7: x0 - x2 <> 0 by A5, ZFMISC_1:def_5; x0 <> x1 by A5, ZFMISC_1:def_5; then [!f,x0,x1,x2!] = ((- (k / (x0 * x1))) - [!f,x1,x2!]) / (x0 - x2) by A1, A2, A3, Th34 .= ((- (k / (x0 * x1))) - (- (k / (x1 * x2)))) / (x0 - x2) by A1, A3, A4, A6, Th34 .= ((- (k / (x0 * x1))) + (k / (x1 * x2))) / (x0 - x2) .= ((- ((k * x2) / ((x0 * x1) * x2))) + (k / (x1 * x2))) / (x0 - x2) by A4, XCMPLX_1:91 .= ((- ((k * x2) / ((x0 * x1) * x2))) + ((k * x0) / (x0 * (x1 * x2)))) / (x0 - x2) by A2, XCMPLX_1:91 .= (- (((k * x2) / ((x0 * x1) * x2)) - ((k * x0) / ((x0 * x1) * x2)))) / (x0 - x2) .= (- (((k * x2) - (k * x0)) / ((x0 * x1) * x2))) / (x0 - x2) by XCMPLX_1:120 .= ((- (k * (x2 - x0))) / ((x0 * x1) * x2)) / (x0 - x2) by XCMPLX_1:187 .= (k * (x0 - x2)) / (((x0 * x1) * x2) * (x0 - x2)) by XCMPLX_1:78 ; hence [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) by A7, XCMPLX_1:91; ::_thesis: verum end; theorem Th36: :: DIFF_2:36 for k, x0, x1, x2, x3 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) proof let k, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) ) assume that A1: for x being Real holds f . x = k / x and A2: x0 <> 0 and A3: ( x1 <> 0 & x2 <> 0 ) and A4: x3 <> 0 ; ::_thesis: ( not x0,x1,x2,x3 are_mutually_different or [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) ) assume A5: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) then A6: x1 <> x2 by ZFMISC_1:def_6; ( x1 <> x3 & x2 <> x3 ) by A5, ZFMISC_1:def_6; then A7: x1,x2,x3 are_mutually_different by A6, ZFMISC_1:def_5; A8: x0 - x3 <> 0 by A5, ZFMISC_1:def_6; ( x0 <> x1 & x0 <> x2 ) by A5, ZFMISC_1:def_6; then x0,x1,x2 are_mutually_different by A6, ZFMISC_1:def_5; then [!f,x0,x1,x2,x3!] = ((k / ((x0 * x1) * x2)) - [!f,x1,x2,x3!]) / (x0 - x3) by A1, A2, A3, Th35 .= ((k / ((x0 * x1) * x2)) - (k / ((x1 * x2) * x3))) / (x0 - x3) by A1, A3, A4, A7, Th35 .= (((k * x3) / (((x0 * x1) * x2) * x3)) - (k / ((x1 * x2) * x3))) / (x0 - x3) by A4, XCMPLX_1:91 .= (((k * x3) / (((x0 * x1) * x2) * x3)) - ((k * x0) / (x0 * ((x1 * x2) * x3)))) / (x0 - x3) by A2, XCMPLX_1:91 .= (((k * x3) - (k * x0)) / (((x0 * x1) * x2) * x3)) / (x0 - x3) by XCMPLX_1:120 .= ((- k) * (x0 - x3)) / ((((x0 * x1) * x2) * x3) * (x0 - x3)) by XCMPLX_1:78 .= (- k) / (((x0 * x1) * x2) * x3) by A8, XCMPLX_1:91 ; hence [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) by XCMPLX_1:187; ::_thesis: verum end; theorem :: DIFF_2:37 for k, x0, x1, x2, x3, x4 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different holds [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) proof let k, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different holds [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different implies [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) ) assume that A1: for x being Real holds f . x = k / x and A2: x0 <> 0 and A3: ( x1 <> 0 & x2 <> 0 & x3 <> 0 ) and A4: x4 <> 0 ; ::_thesis: ( not x0,x1,x2,x3,x4 are_mutually_different or [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) ) assume A5: x0,x1,x2,x3,x4 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) then A6: ( x1 <> x2 & x1 <> x3 ) by ZFMISC_1:def_7; A7: x3 <> x4 by A5, ZFMISC_1:def_7; A8: x2 <> x3 by A5, ZFMISC_1:def_7; A9: x0 - x4 <> 0 by A5, ZFMISC_1:def_7; A10: x0 <> x3 by A5, ZFMISC_1:def_7; ( x1 <> x4 & x2 <> x4 ) by A5, ZFMISC_1:def_7; then A11: x1,x2,x3,x4 are_mutually_different by A6, A8, A7, ZFMISC_1:def_6; ( x0 <> x1 & x0 <> x2 ) by A5, ZFMISC_1:def_7; then x0,x1,x2,x3 are_mutually_different by A10, A6, A8, ZFMISC_1:def_6; then [!f,x0,x1,x2,x3,x4!] = ((- (k / (((x0 * x1) * x2) * x3))) - [!f,x1,x2,x3,x4!]) / (x0 - x4) by A1, A2, A3, Th36 .= ((- (k / (((x0 * x1) * x2) * x3))) - (- (k / (((x1 * x2) * x3) * x4)))) / (x0 - x4) by A1, A3, A4, A11, Th36 .= ((- (k / (((x0 * x1) * x2) * x3))) + (k / (((x1 * x2) * x3) * x4))) / (x0 - x4) .= ((- ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) + (k / (((x1 * x2) * x3) * x4))) / (x0 - x4) by A4, XCMPLX_1:91 .= ((- ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) + ((k * x0) / (x0 * (((x1 * x2) * x3) * x4)))) / (x0 - x4) by A2, XCMPLX_1:91 .= (((k * x0) / ((((x0 * x1) * x2) * x3) * x4)) - ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) / (x0 - x4) .= (((k * x0) - (k * x4)) / ((((x0 * x1) * x2) * x3) * x4)) / (x0 - x4) by XCMPLX_1:120 .= (k * (x0 - x4)) / (((((x0 * x1) * x2) * x3) * x4) * (x0 - x4)) by XCMPLX_1:78 ; hence [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) by A9, XCMPLX_1:91; ::_thesis: verum end; theorem :: DIFF_2:38 for k, h being Real for f being Function of REAL,REAL st ( for x being Real holds ( f . x = k / x & x <> 0 & x + h <> 0 ) ) holds for x being Real holds (fD (f,h)) . x = (- (k * h)) / ((x + h) * x) ; theorem :: DIFF_2:39 for k, h being Real for f being Function of REAL,REAL st ( for x being Real holds ( f . x = k / x & x <> 0 & x - h <> 0 ) ) holds for x being Real holds (bD (f,h)) . x = (- (k * h)) / ((x - h) * x) ; theorem :: DIFF_2:40 for k, h being Real for f being Function of REAL,REAL st ( for x being Real holds ( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) holds for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) proof let k, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds ( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) holds for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds ( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) implies for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ) assume A1: for x being Real holds ( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ; ::_thesis: for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) let x be Real; ::_thesis: (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) A2: x + (h / 2) <> 0 by A1; A3: x - (h / 2) <> 0 by A1; (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5 .= (k / (x + (h / 2))) - (f . (x - (h / 2))) by A1 .= (k / (x + (h / 2))) - (k / (x - (h / 2))) by A1 .= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - (k / (x - (h / 2))) by A3, XCMPLX_1:91 .= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - ((k * (x + (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) by A2, XCMPLX_1:91 .= (((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2))) by XCMPLX_1:120 ; hence (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_2:41 for x0, x1 being Real holds [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1) [!sin,x0,x1!] = ((sin x0) - (sin x1)) / (x0 - x1) .= (2 * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) / (x0 - x1) by SIN_COS4:16 ; hence [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_2:42 for h, x being Real holds (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))) proof let h, x be Real; ::_thesis: (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))) (fD (sin,h)) . x = (sin (x + h)) - (sin x) by DIFF_1:3 .= 2 * ((cos ((x + (h + x)) / 2)) * (sin (((x + h) - x) / 2))) by SIN_COS4:16 ; hence (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_2:43 for h, x being Real holds (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))) proof let h, x be Real; ::_thesis: (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))) (bD (sin,h)) . x = (sin x) - (sin (x - h)) by DIFF_1:4 .= 2 * ((cos ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2))) by SIN_COS4:16 ; hence (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_2:44 for h, x being Real holds (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2))) proof let h, x be Real; ::_thesis: (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2))) (cD (sin,h)) . x = (sin (x + (h / 2))) - (sin (x - (h / 2))) by DIFF_1:5 .= 2 * ((cos (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2))) by SIN_COS4:16 ; hence (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_2:45 for x0, x1 being Real holds [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)) proof let x0, x1 be Real; ::_thesis: [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)) [!cos,x0,x1!] = ((cos x0) - (cos x1)) / (x0 - x1) .= (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1) by SIN_COS4:18 ; hence [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)) by XCMPLX_1:187; ::_thesis: verum end; theorem :: DIFF_2:46 for h, x being Real holds (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) proof let h, x be Real; ::_thesis: (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) (fD (cos,h)) . x = (cos (x + h)) - (cos x) by DIFF_1:3 .= - (2 * ((sin ((x + (x + h)) / 2)) * (sin (((x + h) - x) / 2)))) by SIN_COS4:18 ; hence (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:47 for h, x being Real holds (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) proof let h, x be Real; ::_thesis: (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) (bD (cos,h)) . x = (cos x) - (cos (x - h)) by DIFF_1:4 .= - (2 * ((sin ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2)))) by SIN_COS4:18 ; hence (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:48 for h, x being Real holds (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2)))) proof let h, x be Real; ::_thesis: (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2)))) (cD (cos,h)) . x = (cos (x + (h / 2))) - (cos (x - (h / 2))) by DIFF_1:5 .= - (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))) by SIN_COS4:18 ; hence (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:49 for x0, x1 being Real holds [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) [!(sin (#) sin),x0,x1!] = (((sin . x0) * (sin . x0)) - ((sin (#) sin) . x1)) / (x0 - x1) by VALUED_1:5 .= (((sin x0) * (sin x0)) - ((sin x1) * (sin x1))) / (x0 - x1) by VALUED_1:5 .= ((- ((1 / 2) * ((cos (x0 + x0)) - (cos (x0 - x0))))) - ((sin x1) * (sin x1))) / (x0 - x1) by SIN_COS4:29 .= ((- ((1 / 2) * ((cos (x0 + x0)) - (cos (x0 - x0))))) - (- ((1 / 2) * ((cos (x1 + x1)) - (cos (x1 - x1)))))) / (x0 - x1) by SIN_COS4:29 .= ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) ; hence [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_2:50 for h, x being Real holds (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h)))) proof let h, x be Real; ::_thesis: (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h)))) (fD ((sin (#) sin),h)) . x = ((sin (#) sin) . (x + h)) - ((sin (#) sin) . x) by DIFF_1:3 .= ((sin . (x + h)) * (sin . (x + h))) - ((sin (#) sin) . x) by VALUED_1:5 .= ((sin (x + h)) * (sin (x + h))) - ((sin x) * (sin x)) by VALUED_1:5 .= (- ((1 / 2) * ((cos ((x + h) + (x + h))) - (cos ((x + h) - (x + h)))))) - ((sin x) * (sin x)) by SIN_COS4:29 .= (- ((1 / 2) * ((cos (2 * (x + h))) - (cos 0)))) - (- ((1 / 2) * ((cos (x + x)) - (cos (x - x))))) by SIN_COS4:29 ; hence (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h)))) ; ::_thesis: verum end; theorem :: DIFF_2:51 for h, x being Real holds (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x))) proof let h, x be Real; ::_thesis: (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x))) (bD ((sin (#) sin),h)) . x = ((sin (#) sin) . x) - ((sin (#) sin) . (x - h)) by DIFF_1:4 .= ((sin . x) * (sin . x)) - ((sin (#) sin) . (x - h)) by VALUED_1:5 .= ((sin x) * (sin x)) - ((sin (x - h)) * (sin (x - h))) by VALUED_1:5 .= (- ((1 / 2) * ((cos (x + x)) - (cos (x - x))))) - ((sin (x - h)) * (sin (x - h))) by SIN_COS4:29 .= (- ((1 / 2) * ((cos (2 * x)) - (cos 0)))) - (- ((1 / 2) * ((cos ((x - h) + (x - h))) - (cos ((x - h) - (x - h)))))) by SIN_COS4:29 ; hence (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x))) ; ::_thesis: verum end; theorem :: DIFF_2:52 for h, x being Real holds (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h))) proof let h, x be Real; ::_thesis: (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h))) (cD ((sin (#) sin),h)) . x = ((sin (#) sin) . (x + (h / 2))) - ((sin (#) sin) . (x - (h / 2))) by DIFF_1:5 .= ((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) - ((sin (#) sin) . (x - (h / 2))) by VALUED_1:5 .= ((sin (x + (h / 2))) * (sin (x + (h / 2)))) - ((sin (x - (h / 2))) * (sin (x - (h / 2)))) by VALUED_1:5 .= (- ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) - (cos ((x + (h / 2)) - (x + (h / 2))))))) - ((sin (x - (h / 2))) * (sin (x - (h / 2)))) by SIN_COS4:29 .= (- ((1 / 2) * ((cos (2 * (x + (h / 2)))) - (cos 0)))) - (- ((1 / 2) * ((cos ((x - (h / 2)) + (x - (h / 2)))) - (cos ((x - (h / 2)) - (x - (h / 2))))))) by SIN_COS4:29 ; hence (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h))) ; ::_thesis: verum end; theorem :: DIFF_2:53 for x0, x1 being Real holds [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) [!(sin (#) cos),x0,x1!] = (((sin . x0) * (cos . x0)) - ((sin (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= (((sin x0) * (cos x0)) - ((sin x1) * (cos x1))) / (x0 - x1) by VALUED_1:5 .= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((sin x1) * (cos x1))) / (x0 - x1) by SIN_COS4:30 .= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((1 / 2) * ((sin (x1 + x1)) + (sin (x1 - x1))))) / (x0 - x1) by SIN_COS4:30 .= ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ; hence [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_2:54 for h, x being Real holds (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x))) proof let h, x be Real; ::_thesis: (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x))) (fD ((sin (#) cos),h)) . x = ((sin (#) cos) . (x + h)) - ((sin (#) cos) . x) by DIFF_1:3 .= ((sin . (x + h)) * (cos . (x + h))) - ((sin (#) cos) . x) by VALUED_1:5 .= ((sin (x + h)) * (cos (x + h))) - ((sin x) * (cos x)) by VALUED_1:5 .= ((1 / 2) * ((sin ((x + h) + (x + h))) + (sin ((x + h) - (x + h))))) - ((sin x) * (cos x)) by SIN_COS4:30 .= ((1 / 2) * ((sin (2 * (x + h))) + (sin 0))) - ((1 / 2) * ((sin (x + x)) + (sin (x - x)))) by SIN_COS4:30 .= ((1 / 2) * (sin (2 * (x + h)))) - ((1 / 2) * (sin (2 * x))) ; hence (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x))) ; ::_thesis: verum end; theorem :: DIFF_2:55 for h, x being Real holds (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h)))) proof let h, x be Real; ::_thesis: (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h)))) (bD ((sin (#) cos),h)) . x = ((sin (#) cos) . x) - ((sin (#) cos) . (x - h)) by DIFF_1:4 .= ((sin . x) * (cos . x)) - ((sin (#) cos) . (x - h)) by VALUED_1:5 .= ((sin x) * (cos x)) - ((sin (x - h)) * (cos (x - h))) by VALUED_1:5 .= ((1 / 2) * ((sin (x + x)) + (sin (x - x)))) - ((sin (x - h)) * (cos (x - h))) by SIN_COS4:30 .= ((1 / 2) * ((sin (x + x)) + (sin 0))) - ((1 / 2) * ((sin ((x - h) + (x - h))) + (sin ((x - h) - (x - h))))) by SIN_COS4:30 .= ((1 / 2) * (sin (2 * x))) - ((1 / 2) * (sin (2 * (x - h)))) ; hence (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h)))) ; ::_thesis: verum end; theorem :: DIFF_2:56 for h, x being Real holds (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h))) proof let h, x be Real; ::_thesis: (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h))) (cD ((sin (#) cos),h)) . x = ((sin (#) cos) . (x + (h / 2))) - ((sin (#) cos) . (x - (h / 2))) by DIFF_1:5 .= ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((sin (#) cos) . (x - (h / 2))) by VALUED_1:5 .= ((sin (x + (h / 2))) * (cos (x + (h / 2)))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by VALUED_1:5 .= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by SIN_COS4:30 .= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((1 / 2) * ((sin ((x - (h / 2)) + (x - (h / 2)))) + (sin ((x - (h / 2)) - (x - (h / 2)))))) by SIN_COS4:30 .= ((1 / 2) * (sin (2 * (x + (h / 2))))) - ((1 / 2) * (sin (2 * (x - (h / 2))))) ; hence (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h))) ; ::_thesis: verum end; theorem :: DIFF_2:57 for x0, x1 being Real holds [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1) [!(cos (#) cos),x0,x1!] = (((cos . x0) * (cos . x0)) - ((cos (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= (((cos x0) * (cos x0)) - ((cos x1) * (cos x1))) / (x0 - x1) by VALUED_1:5 .= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((cos x1) * (cos x1))) / (x0 - x1) by SIN_COS4:32 .= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((1 / 2) * ((cos (x1 + x1)) + (cos (x1 - x1))))) / (x0 - x1) by SIN_COS4:32 .= (((1 / 2) * (cos (2 * x0))) - ((1 / 2) * (cos (2 * x1)))) / (x0 - x1) ; hence [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_2:58 for h, x being Real holds (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x))) proof let h, x be Real; ::_thesis: (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x))) (fD ((cos (#) cos),h)) . x = ((cos (#) cos) . (x + h)) - ((cos (#) cos) . x) by DIFF_1:3 .= ((cos . (x + h)) * (cos . (x + h))) - ((cos (#) cos) . x) by VALUED_1:5 .= ((cos (x + h)) * (cos (x + h))) - ((cos x) * (cos x)) by VALUED_1:5 .= ((1 / 2) * ((cos ((x + h) + (x + h))) + (cos ((x + h) - (x + h))))) - ((cos x) * (cos x)) by SIN_COS4:32 .= ((1 / 2) * ((cos (2 * (x + h))) + (cos 0))) - ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) by SIN_COS4:32 .= ((1 / 2) * (cos (2 * (x + h)))) - ((1 / 2) * (cos (2 * x))) ; hence (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x))) ; ::_thesis: verum end; theorem :: DIFF_2:59 for h, x being Real holds (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h)))) proof let h, x be Real; ::_thesis: (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h)))) (bD ((cos (#) cos),h)) . x = ((cos (#) cos) . x) - ((cos (#) cos) . (x - h)) by DIFF_1:4 .= ((cos . x) * (cos . x)) - ((cos (#) cos) . (x - h)) by VALUED_1:5 .= ((cos x) * (cos x)) - ((cos (x - h)) * (cos (x - h))) by VALUED_1:5 .= ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) - ((cos (x - h)) * (cos (x - h))) by SIN_COS4:32 .= ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) - ((1 / 2) * ((cos ((x - h) + (x - h))) + (cos ((x - h) - (x - h))))) by SIN_COS4:32 .= ((1 / 2) * (cos (2 * x))) - ((1 / 2) * (cos (2 * (x - h)))) ; hence (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h)))) ; ::_thesis: verum end; theorem :: DIFF_2:60 for h, x being Real holds (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h))) proof let h, x be Real; ::_thesis: (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h))) (cD ((cos (#) cos),h)) . x = ((cos (#) cos) . (x + (h / 2))) - ((cos (#) cos) . (x - (h / 2))) by DIFF_1:5 .= ((cos . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cos (#) cos) . (x - (h / 2))) by VALUED_1:5 .= ((cos (x + (h / 2))) * (cos (x + (h / 2)))) - ((cos (x - (h / 2))) * (cos (x - (h / 2)))) by VALUED_1:5 .= ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) + (cos ((x + (h / 2)) - (x + (h / 2)))))) - ((cos (x - (h / 2))) * (cos (x - (h / 2)))) by SIN_COS4:32 .= ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) + (cos ((x + (h / 2)) - (x + (h / 2)))))) - ((1 / 2) * ((cos ((x - (h / 2)) + (x - (h / 2)))) + (cos ((x - (h / 2)) - (x - (h / 2)))))) by SIN_COS4:32 .= ((1 / 2) * (cos (2 * (x + (h / 2))))) - ((1 / 2) * (cos (2 * (x - (h / 2))))) ; hence (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h))) ; ::_thesis: verum end; theorem :: DIFF_2:61 for x0, x1 being Real holds [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1)) proof let x0, x1 be Real; ::_thesis: [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1)) set y = 3 * x0; set z = 3 * x1; [!((sin (#) sin) (#) cos),x0,x1!] = ((((sin (#) sin) . x0) * (cos . x0)) - (((sin (#) sin) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) * (sin . x0)) * (cos . x0)) - (((sin (#) sin) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) * (sin . x0)) * (cos . x0)) - (((sin (#) sin) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= ((((sin x0) * (sin x0)) * (cos x0)) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5 .= (((1 / 4) * ((((- (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) - (cos ((x0 + x0) + x0)))) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:34 .= (((1 / 4) * ((cos x0) - (cos (3 * x0)))) - ((1 / 4) * ((((- (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) - (cos ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:34 .= (((1 / 4) * ((cos x0) - (cos x1))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1) .= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1) by SIN_COS4:18 .= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * (- (2 * ((sin (((3 * x1) + (3 * x0)) / 2)) * (sin (((3 * x1) - (3 * x0)) / 2))))))) / (x0 - x1) by SIN_COS4:18 .= (- ((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) / (x0 - x1) ; hence [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1)) by XCMPLX_1:187; ::_thesis: verum end; theorem :: DIFF_2:62 for h, x being Real holds (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) proof let h, x be Real; ::_thesis: (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) set y = 3 * x; set z = 3 * h; (fD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . (x + h)) - (((sin (#) sin) (#) cos) . x) by DIFF_1:3 .= (((sin (#) sin) . (x + h)) * (cos . (x + h))) - (((sin (#) sin) (#) cos) . x) by VALUED_1:5 .= (((sin . (x + h)) * (sin . (x + h))) * (cos . (x + h))) - (((sin (#) sin) (#) cos) . x) by VALUED_1:5 .= (((sin . (x + h)) * (sin . (x + h))) * (cos . (x + h))) - (((sin (#) sin) . x) * (cos . x)) by VALUED_1:5 .= (((sin (x + h)) * (sin (x + h))) * (cos (x + h))) - (((sin x) * (sin x)) * (cos x)) by VALUED_1:5 .= ((1 / 4) * ((((- (cos (((x + h) + (x + h)) - (x + h)))) + (cos (((x + h) + (x + h)) - (x + h)))) + (cos (((x + h) + (x + h)) - (x + h)))) - (cos (((x + h) + (x + h)) + (x + h))))) - (((sin x) * (sin x)) * (cos x)) by SIN_COS4:34 .= ((1 / 4) * ((cos (x + h)) - (cos (3 * (x + h))))) - ((1 / 4) * ((((- (cos ((x + x) - x))) + (cos ((x + x) - x))) + (cos ((x + x) - x))) - (cos ((x + x) + x)))) by SIN_COS4:34 .= ((1 / 4) * ((cos (x + h)) - (cos x))) - ((1 / 4) * ((cos (3 * (x + h))) - (cos (3 * x)))) .= ((1 / 4) * (- (2 * ((sin (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2)))))) - ((1 / 4) * ((cos (3 * (x + h))) - (cos (3 * x)))) by SIN_COS4:18 .= ((1 / 4) * (- (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin ((((3 * x) + (3 * h)) + (3 * x)) / 2)) * (sin ((((3 * x) + (3 * h)) - (3 * x)) / 2)))))) by SIN_COS4:18 .= ((1 / 2) * ((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ; hence (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:63 for h, x being Real holds (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) proof let h, x be Real; ::_thesis: (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) set y = 3 * x; set z = 3 * h; (bD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . x) - (((sin (#) sin) (#) cos) . (x - h)) by DIFF_1:4 .= (((sin (#) sin) . x) * (cos . x)) - (((sin (#) sin) (#) cos) . (x - h)) by VALUED_1:5 .= (((sin . x) * (sin . x)) * (cos . x)) - (((sin (#) sin) (#) cos) . (x - h)) by VALUED_1:5 .= (((sin . x) * (sin . x)) * (cos . x)) - (((sin (#) sin) . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= (((sin x) * (sin x)) * (cos x)) - (((sin (x - h)) * (sin (x - h))) * (cos (x - h))) by VALUED_1:5 .= ((1 / 4) * ((((- (cos ((x + x) - x))) + (cos ((x + x) - x))) + (cos ((x + x) - x))) - (cos ((x + x) + x)))) - (((sin (x - h)) * (sin (x - h))) * (cos (x - h))) by SIN_COS4:34 .= ((1 / 4) * ((cos x) - (cos (3 * x)))) - ((1 / 4) * ((((- (cos (((x - h) + (x - h)) - (x - h)))) + (cos (((x - h) + (x - h)) - (x - h)))) + (cos (((x - h) + (x - h)) - (x - h)))) - (cos (((x - h) + (x - h)) + (x - h))))) by SIN_COS4:34 .= ((1 / 4) * ((cos x) - (cos (x - h)))) - ((1 / 4) * ((cos (3 * x)) - (cos (3 * (x - h))))) .= ((1 / 4) * (- (2 * ((sin ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2)))))) - ((1 / 4) * ((cos (3 * x)) - (cos (3 * (x - h))))) by SIN_COS4:18 .= ((1 / 4) * (- (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin (((3 * x) + ((3 * x) - (3 * h))) / 2)) * (sin (((3 * x) - ((3 * x) - (3 * h))) / 2)))))) by SIN_COS4:18 .= ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ; hence (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:64 for h, x being Real holds (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) proof let h, x be Real; ::_thesis: (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) set y = 3 * x; set z = 3 * h; (cD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . (x + (h / 2))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by DIFF_1:5 .= (((sin (#) sin) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= (((sin (x + (h / 2))) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by VALUED_1:5 .= ((1 / 4) * ((((- (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) - (cos (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by SIN_COS4:34 .= ((1 / 4) * ((cos (x + (h / 2))) - (cos (3 * (x + (h / 2)))))) - ((1 / 4) * ((((- (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) - (cos (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2)))))) by SIN_COS4:34 .= ((1 / 4) * ((cos (x + (h / 2))) - (cos (x - (h / 2))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2)))))) .= ((1 / 4) * (- (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2)))))) by SIN_COS4:18 .= ((1 / 4) * (- (2 * ((sin x) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin ((((3 * x) + ((3 * h) / 2)) + ((3 * x) - ((3 * h) / 2))) / 2)) * (sin ((((3 * x) + ((3 * h) / 2)) - ((3 * x) - ((3 * h) / 2))) / 2)))))) by SIN_COS4:18 .= (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ; hence (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:65 for x0, x1 being Real holds [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) set y = 3 * x0; set z = 3 * x1; [!((sin (#) cos) (#) cos),x0,x1!] = ((((sin (#) cos) . x0) * (cos . x0)) - (((sin (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) * (cos . x0)) * (cos . x0)) - (((sin (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) * (cos . x0)) * (cos . x0)) - (((sin (#) cos) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= ((((sin x0) * (cos x0)) * (cos x0)) - (((sin x1) * (cos x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5 .= (((1 / 4) * ((((sin ((x0 + x0) - x0)) - (sin ((x0 + x0) - x0))) + (sin ((x0 + x0) - x0))) + (sin ((x0 + x0) + x0)))) - (((sin x1) * (cos x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:35 .= (((1 / 4) * ((sin x0) + (sin (3 * x0)))) - ((1 / 4) * ((((sin ((x1 + x1) - x1)) - (sin ((x1 + x1) - x1))) + (sin ((x1 + x1) - x1))) + (sin ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:35 .= (((1 / 4) * ((sin x0) - (sin x1))) + ((1 / 4) * ((sin (3 * x0)) - (sin (3 * x1))))) / (x0 - x1) .= (((1 / 4) * (2 * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) + ((1 / 4) * ((sin (3 * x0)) - (sin (3 * x1))))) / (x0 - x1) by SIN_COS4:16 .= (((1 / 2) * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) + ((1 / 4) * (2 * ((cos (((3 * x0) + (3 * x1)) / 2)) * (sin (((3 * x0) - (3 * x1)) / 2)))))) / (x0 - x1) by SIN_COS4:16 .= ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) ; hence [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_2:66 for h, x being Real holds (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) proof let h, x be Real; ::_thesis: (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) set y = 3 * x; set z = 3 * h; (fD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . (x + h)) - (((sin (#) cos) (#) cos) . x) by DIFF_1:3 .= (((sin (#) cos) . (x + h)) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5 .= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5 .= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) . x) * (cos . x)) by VALUED_1:5 .= (((sin (x + h)) * (cos (x + h))) * (cos (x + h))) - (((sin x) * (cos x)) * (cos x)) by VALUED_1:5 .= ((1 / 4) * ((((sin (((x + h) + (x + h)) - (x + h))) - (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) + (x + h))))) - (((sin x) * (cos x)) * (cos x)) by SIN_COS4:35 .= ((1 / 4) * ((sin (x + h)) + (sin (3 * (x + h))))) - ((1 / 4) * ((((sin ((x + x) - x)) - (sin ((x + x) - x))) + (sin ((x + x) - x))) + (sin ((x + x) + x)))) by SIN_COS4:35 .= ((1 / 4) * ((sin (x + h)) - (sin x))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x)))) .= ((1 / 4) * (2 * ((cos (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2))))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x)))) by SIN_COS4:16 .= ((1 / 4) * (2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos ((((3 * x) + (3 * h)) + (3 * x)) / 2)) * (sin ((((3 * x) + (3 * h)) - (3 * x)) / 2))))) by SIN_COS4:16 .= ((1 / 2) * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))) + ((1 / 2) * ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; hence (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:67 for h, x being Real holds (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) proof let h, x be Real; ::_thesis: (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) set y = 3 * x; set z = 3 * h; (bD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . x) - (((sin (#) cos) (#) cos) . (x - h)) by DIFF_1:4 .= (((sin (#) cos) . x) * (cos . x)) - (((sin (#) cos) (#) cos) . (x - h)) by VALUED_1:5 .= (((sin . x) * (cos . x)) * (cos . x)) - (((sin (#) cos) (#) cos) . (x - h)) by VALUED_1:5 .= (((sin . x) * (cos . x)) * (cos . x)) - (((sin (#) cos) . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= (((sin x) * (cos x)) * (cos x)) - (((sin (x - h)) * (cos (x - h))) * (cos (x - h))) by VALUED_1:5 .= ((1 / 4) * ((((sin ((x + x) - x)) - (sin ((x + x) - x))) + (sin ((x + x) - x))) + (sin ((x + x) + x)))) - (((sin (x - h)) * (cos (x - h))) * (cos (x - h))) by SIN_COS4:35 .= ((1 / 4) * ((sin x) + (sin (3 * x)))) - ((1 / 4) * ((((sin (((x - h) + (x - h)) - (x - h))) - (sin (((x - h) + (x - h)) - (x - h)))) + (sin (((x - h) + (x - h)) - (x - h)))) + (sin (((x - h) + (x - h)) + (x - h))))) by SIN_COS4:35 .= ((1 / 4) * ((sin x) - (sin (x - h)))) + ((1 / 4) * ((sin (3 * x)) - (sin (3 * (x - h))))) .= ((1 / 4) * (2 * ((cos ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2))))) + ((1 / 4) * ((sin (3 * x)) - (sin (3 * (x - h))))) by SIN_COS4:16 .= ((1 / 4) * (2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos (((3 * x) + ((3 * x) - (3 * h))) / 2)) * (sin (((3 * x) - ((3 * x) - (3 * h))) / 2))))) by SIN_COS4:16 .= ((1 / 2) * ((cos (((2 * x) - h) / 2)) * (sin (h / 2)))) + ((1 / 2) * ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; hence (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:68 for h, x being Real holds (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2)))) proof let h, x be Real; ::_thesis: (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2)))) set y = 3 * x; set z = 3 * h; (cD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . (x + (h / 2))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by DIFF_1:5 .= (((sin (#) cos) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) cos) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= (((sin (x + (h / 2))) * (cos (x + (h / 2)))) * (cos (x + (h / 2)))) - (((sin (x - (h / 2))) * (cos (x - (h / 2)))) * (cos (x - (h / 2)))) by VALUED_1:5 .= ((1 / 4) * ((((sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2)))) - (sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (sin (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - (((sin (x - (h / 2))) * (cos (x - (h / 2)))) * (cos (x - (h / 2)))) by SIN_COS4:35 .= ((1 / 4) * ((sin (x + (h / 2))) + (sin (3 * (x + (h / 2)))))) - ((1 / 4) * ((((sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2)))) - (sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (sin (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2)))))) by SIN_COS4:35 .= ((1 / 4) * ((sin (x + (h / 2))) - (sin (x - (h / 2))))) + ((1 / 4) * ((sin (3 * (x + (h / 2)))) - (sin (3 * (x - (h / 2)))))) .= ((1 / 4) * (2 * ((cos (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2))))) + ((1 / 4) * ((sin (3 * (x + (h / 2)))) - (sin (3 * (x - (h / 2)))))) by SIN_COS4:16 .= ((1 / 4) * (2 * ((cos x) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos ((((3 * x) + ((3 * h) / 2)) + ((3 * x) - ((3 * h) / 2))) / 2)) * (sin ((((3 * x) + ((3 * h) / 2)) - ((3 * x) - ((3 * h) / 2))) / 2))))) by SIN_COS4:16 .= ((1 / 2) * ((cos x) * (sin (h / 2)))) + ((1 / 2) * ((cos (3 * x)) * (sin ((3 * h) / 2)))) ; hence (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum end; theorem :: DIFF_2:69 for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) ) assume that A1: x0 in dom tan and A2: x1 in dom tan ; ::_thesis: [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) A3: tan . x0 = (sin . x0) * ((cos . x0) ") by A1, RFUNCT_1:def_1 .= (sin . x0) * (1 / (cos . x0)) by XCMPLX_1:215 .= tan x0 by XCMPLX_1:99 ; A4: tan . x1 = (sin . x1) * ((cos . x1) ") by A2, RFUNCT_1:def_1 .= (sin . x1) * (1 / (cos . x1)) by XCMPLX_1:215 .= tan x1 by XCMPLX_1:99 ; ( cos x0 <> 0 & cos x1 <> 0 ) by A1, A2, FDIFF_8:1; then [!tan,x0,x1!] = ((sin (x0 - x1)) / ((cos x0) * (cos x1))) / (x0 - x1) by A3, A4, SIN_COS4:20 .= (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) by XCMPLX_1:78 ; hence [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_2:70 for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) proof let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) ) assume that A1: x0 in dom cot and A2: x1 in dom cot ; ::_thesis: [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) A3: cot . x0 = (cos . x0) * ((sin . x0) ") by A1, RFUNCT_1:def_1 .= (cos . x0) * (1 / (sin . x0)) by XCMPLX_1:215 .= cot x0 by XCMPLX_1:99 ; A4: cot . x1 = (cos . x1) * ((sin . x1) ") by A2, RFUNCT_1:def_1 .= (cos . x1) * (1 / (sin . x1)) by XCMPLX_1:215 .= cot x1 by XCMPLX_1:99 ; ( sin x0 <> 0 & sin x1 <> 0 ) by A1, A2, FDIFF_8:2; then [!cot,x0,x1!] = (- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) / (x0 - x1) by A3, A4, SIN_COS4:24 .= - (((sin (x0 - x1)) / ((sin x0) * (sin x1))) / (x0 - x1)) by XCMPLX_1:187 ; hence [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) by XCMPLX_1:78; ::_thesis: verum end; theorem :: DIFF_2:71 for x0, x1 being Real st x0 in dom cosec & x1 in dom cosec holds [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom cosec & x1 in dom cosec implies [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) ) assume that A1: x0 in dom cosec and A2: x1 in dom cosec ; ::_thesis: [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) A3: cosec . x1 = (sin . x1) " by A2, RFUNCT_1:def_2 .= cosec x1 by XCMPLX_1:215 ; cosec . x0 = (sin . x0) " by A1, RFUNCT_1:def_2 .= cosec x0 by XCMPLX_1:215 ; then [!cosec,x0,x1!] = (((1 * (sin x1)) / ((sin x0) * (sin x1))) - (1 / (sin x1))) / (x0 - x1) by A2, A3, RFUNCT_1:3, XCMPLX_1:91 .= (((1 * (sin x1)) / ((sin x0) * (sin x1))) - ((1 * (sin x0)) / ((sin x1) * (sin x0)))) / (x0 - x1) by A1, RFUNCT_1:3, XCMPLX_1:91 .= (((sin x1) - (sin x0)) / ((sin x1) * (sin x0))) / (x0 - x1) by XCMPLX_1:120 .= ((sin x1) - (sin x0)) / (((sin x1) * (sin x0)) * (x0 - x1)) by XCMPLX_1:78 .= (2 * ((cos ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((sin x1) * (sin x0)) * (x0 - x1)) by SIN_COS4:16 ; hence [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_2:72 for x0, x1 being Real st x0 in dom sec & x1 in dom sec holds [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) proof let x0, x1 be Real; ::_thesis: ( x0 in dom sec & x1 in dom sec implies [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) ) assume that A1: x0 in dom sec and A2: x1 in dom sec ; ::_thesis: [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) A3: sec . x1 = (cos . x1) " by A2, RFUNCT_1:def_2 .= sec x1 by XCMPLX_1:215 ; sec . x0 = (cos . x0) " by A1, RFUNCT_1:def_2 .= sec x0 by XCMPLX_1:215 ; then [!sec,x0,x1!] = (((1 * (cos x1)) / ((cos x0) * (cos x1))) - (1 / (cos x1))) / (x0 - x1) by A2, A3, RFUNCT_1:3, XCMPLX_1:91 .= (((1 * (cos x1)) / ((cos x0) * (cos x1))) - ((1 * (cos x0)) / ((cos x1) * (cos x0)))) / (x0 - x1) by A1, RFUNCT_1:3, XCMPLX_1:91 .= (((cos x1) - (cos x0)) / ((cos x1) * (cos x0))) / (x0 - x1) by XCMPLX_1:120 .= ((cos x1) - (cos x0)) / (((cos x1) * (cos x0)) * (x0 - x1)) by XCMPLX_1:78 .= (- (2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2))))) / (((cos x1) * (cos x0)) * (x0 - x1)) by SIN_COS4:18 .= - ((2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((cos x1) * (cos x0)) * (x0 - x1))) by XCMPLX_1:187 ; hence [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) ; ::_thesis: verum end;