let x0, x1, x2 be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x0,x1,x2 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 holds
[!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2))))
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = sqrt x ) & x0,x1,x2 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 implies [!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2)))) )
assume that
A1: for x being Real holds f . x = sqrt x and
A2: x0,x1,x2 are_mutually_distinct and
A3: ( x0 > 0 & x1 > 0 & x2 > 0 ) ; :: thesis: [!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2))))
A4: ( f . x0 = sqrt x0 & f . x1 = sqrt x1 & f . x2 = sqrt x2 ) by A1;
( sqrt x0 > 0 & sqrt x1 > 0 & sqrt x2 > 0 ) by A3, SQUARE_1:25;
then A5: ( (sqrt x0) + (sqrt x1) > 0 & (sqrt x1) + (sqrt x2) > 0 ) ;
A6: ( x0 <> x1 & x1 <> x2 & x2 <> x0 ) by A2, ZFMISC_1:def 5;
then [!f,x0,x1,x2!] = ((1 / ((sqrt x0) + (sqrt x1))) - (((sqrt x1) - (sqrt x2)) / (x1 - x2))) / (x0 - x2) by A3, A4, SQUARE_1:36
.= ((1 / ((sqrt x0) + (sqrt x1))) - (1 / ((sqrt x1) + (sqrt x2)))) / (x0 - x2) by A3, A6, SQUARE_1:36
.= (((1 * ((sqrt x1) + (sqrt x2))) - (1 * ((sqrt x0) + (sqrt x1)))) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (x0 - x2) by A5, XCMPLX_1:130
.= (((sqrt x2) - (sqrt x0)) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (- (x2 - x0))
.= - ((((sqrt x2) - (sqrt x0)) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (x2 - x0)) by XCMPLX_1:188
.= - ((1 / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) * (((sqrt x2) - (sqrt x0)) / (x2 - x0)))
.= - ((1 / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) * (1 / ((sqrt x2) + (sqrt x0)))) by A3, A6, SQUARE_1:36
.= - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) by XCMPLX_1:102 ;
hence [!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2)))) ; :: thesis: verum