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_different & 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_different & 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_different 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;
A5: ( sqrt x0 > 0 & sqrt x1 > 0 & sqrt x2 > 0 ) by A3, SQUARE_1:93;
A6: ( (sqrt x0) + (sqrt x1) > 0 & (sqrt x1) + (sqrt x2) > 0 ) by A5, XREAL_1:36;
A7: ( x0 <> x1 & x1 <> x2 & x2 <> x0 ) by A2, ZFMISC_1:def 5;
[!f,x0,x1,x2!] = ((1 / ((sqrt x0) + (sqrt x1))) - (((sqrt x1) - (sqrt x2)) / (x1 - x2))) / (x0 - x2) by A3, A4, A7, SQUARE_1:105
.= ((1 / ((sqrt x0) + (sqrt x1))) - (1 / ((sqrt x1) + (sqrt x2)))) / (x0 - x2) by A3, A7, SQUARE_1:105
.= (((1 * ((sqrt x1) + (sqrt x2))) - (1 * ((sqrt x0) + (sqrt x1)))) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (x0 - x2) by A6, XCMPLX_1:131
.= (((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:189
.= - ((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, A7, SQUARE_1:105
.= - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) by XCMPLX_1:103 ;
hence [!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2)))) ; :: thesis: verum