let x0, x1, x2, x3 be Real; for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x0,x1,x2,x3 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 holds
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
let f be Function of REAL,REAL; ( ( for x being Real holds f . x = sqrt x ) & x0,x1,x2,x3 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 implies [!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3))) )
assume that
A1:
for x being Real holds f . x = sqrt x
and
A2:
x0,x1,x2,x3 are_mutually_distinct
and
A3:
( x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 )
; [!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
A4:
( f . x0 = sqrt x0 & f . x1 = sqrt x1 & f . x2 = sqrt x2 & f . x3 = sqrt x3 )
by A1;
( sqrt x0 > 0 & sqrt x1 > 0 & sqrt x2 > 0 & sqrt x3 > 0 )
by A3, SQUARE_1:25;
then A5:
( (sqrt x0) + (sqrt x1) > 0 & (sqrt x1) + (sqrt x2) > 0 & (sqrt x2) + (sqrt x3) > 0 & (sqrt x2) + (sqrt x0) > 0 & (sqrt x3) + (sqrt x1) > 0 )
;
A6:
( x0 <> x1 & x0 <> x2 & x0 <> x3 & x1 <> x2 & x1 <> x3 & x2 <> x3 )
by A2, ZFMISC_1:def 6;
then [!f,x0,x1,x2,x3!] =
((((1 / ((sqrt x0) + (sqrt x1))) - (((sqrt x1) - (sqrt x2)) / (x1 - x2))) / (x0 - x2)) - (((((sqrt x1) - (sqrt x2)) / (x1 - x2)) - (((sqrt x2) - (sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by A3, A4, SQUARE_1:36
.=
((((1 / ((sqrt x0) + (sqrt x1))) - (1 / ((sqrt x1) + (sqrt x2)))) / (x0 - x2)) - (((((sqrt x1) - (sqrt x2)) / (x1 - x2)) - (((sqrt x2) - (sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by A3, A6, SQUARE_1:36
.=
((((1 / ((sqrt x0) + (sqrt x1))) - (1 / ((sqrt x1) + (sqrt x2)))) / (x0 - x2)) - (((1 / ((sqrt x1) + (sqrt x2))) - (((sqrt x2) - (sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by A3, A6, SQUARE_1:36
.=
((((1 / ((sqrt x0) + (sqrt x1))) - (1 / ((sqrt x1) + (sqrt x2)))) / (x0 - x2)) - (((1 / ((sqrt x1) + (sqrt x2))) - (1 / ((sqrt x2) + (sqrt x3)))) / (x1 - x3))) / (x0 - x3)
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)) - (((1 / ((sqrt x1) + (sqrt x2))) - (1 / ((sqrt x2) + (sqrt x3)))) / (x1 - x3))) / (x0 - x3)
by A5, XCMPLX_1:130
.=
(((((1 * ((sqrt x1) + (sqrt x2))) - (1 * ((sqrt x0) + (sqrt x1)))) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (x0 - x2)) - ((((1 * ((sqrt x2) + (sqrt x3))) - (1 * ((sqrt x1) + (sqrt x2)))) / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) / (x1 - x3))) / (x0 - x3)
by A5, XCMPLX_1:130
.=
(((((sqrt x2) - (sqrt x0)) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (- (x2 - x0))) - ((((sqrt x3) - (sqrt x1)) / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) / (- (x3 - x1)))) / (x0 - x3)
.=
((- ((((sqrt x2) - (sqrt x0)) / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) / (x2 - x0))) - ((((sqrt x3) - (sqrt x1)) / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) / (- (x3 - x1)))) / (x0 - x3)
by XCMPLX_1:188
.=
((- ((1 / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) * (((sqrt x2) - (sqrt x0)) / (x2 - x0)))) - (- ((((sqrt x3) - (sqrt x1)) / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) / (x3 - x1)))) / (x0 - x3)
by XCMPLX_1:188
.=
((- ((1 / (((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2)))) * (1 / ((sqrt x2) + (sqrt x0))))) - (- ((((sqrt x3) - (sqrt x1)) / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) / (x3 - x1)))) / (x0 - x3)
by A3, A6, SQUARE_1:36
.=
((- (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))) + ((1 / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) * (((sqrt x3) - (sqrt x1)) / (x3 - x1)))) / (x0 - x3)
by XCMPLX_1:102
.=
((- (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))) + ((1 / (((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3)))) * (1 / ((sqrt x3) + (sqrt x1))))) / (x0 - x3)
by A3, A6, SQUARE_1:36
.=
((1 / ((((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3))) * ((sqrt x3) + (sqrt x1)))) - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))) / (x0 - x3)
by XCMPLX_1:102
.=
(((1 * ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) - (1 * ((((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3))) * ((sqrt x3) + (sqrt x1))))) / (((((sqrt x1) + (sqrt x2)) * ((sqrt x2) + (sqrt x3))) * ((sqrt x3) + (sqrt x1))) * ((((sqrt x0) + (sqrt x1)) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))) / (x0 - x3)
by A5, XCMPLX_1:130
.=
((((((sqrt x0) + (sqrt x1)) * ((sqrt x2) + (sqrt x0))) - (((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1)))) * ((sqrt x1) + (sqrt x2))) / (((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))) * ((sqrt x1) + (sqrt x2)))) / (x0 - x3)
.=
(((((((sqrt x0) * (sqrt x2)) + ((sqrt x0) * (sqrt x0))) + ((sqrt x1) * (sqrt x2))) + ((sqrt x1) * (sqrt x0))) - (((((sqrt x2) * (sqrt x3)) + ((sqrt x2) * (sqrt x1))) + ((sqrt x3) * (sqrt x3))) + ((sqrt x3) * (sqrt x1)))) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) / (x0 - x3)
by A5, XCMPLX_1:91
.=
(((((((sqrt x0) * (sqrt x2)) + (sqrt (x0 ^2))) + ((sqrt x1) * (sqrt x2))) + ((sqrt x1) * (sqrt x0))) - (((((sqrt x2) * (sqrt x3)) + ((sqrt x2) * (sqrt x1))) + ((sqrt x3) * (sqrt x3))) + ((sqrt x3) * (sqrt x1)))) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) / (x0 - x3)
by A3, SQUARE_1:29
.=
(((((((sqrt x0) * (sqrt x2)) + x0) + ((sqrt x1) * (sqrt x2))) + ((sqrt x1) * (sqrt x0))) - (((((sqrt x2) * (sqrt x3)) + ((sqrt x2) * (sqrt x1))) + ((sqrt x3) * (sqrt x3))) + ((sqrt x3) * (sqrt x1)))) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) / (x0 - x3)
by A3, SQUARE_1:22
.=
(((((((sqrt x0) * (sqrt x2)) + x0) + ((sqrt x1) * (sqrt x2))) + ((sqrt x1) * (sqrt x0))) - (((((sqrt x2) * (sqrt x3)) + ((sqrt x2) * (sqrt x1))) + (sqrt (x3 ^2))) + ((sqrt x3) * (sqrt x1)))) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) / (x0 - x3)
by A3, SQUARE_1:29
.=
(((((((sqrt x0) * (sqrt x2)) + x0) + ((sqrt x1) * (sqrt x2))) + ((sqrt x1) * (sqrt x0))) - (((((sqrt x2) * (sqrt x3)) + ((sqrt x2) * (sqrt x1))) + x3) + ((sqrt x3) * (sqrt x1)))) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0)))) / (x0 - x3)
by A3, SQUARE_1:22
.=
((((sqrt x2) + (sqrt x1)) * ((sqrt x0) - (sqrt x3))) + (x0 - x3)) / (((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))) * (x0 - x3))
by XCMPLX_1:78
.=
((((sqrt x0) - (sqrt x3)) * ((sqrt x2) + (sqrt x1))) + (((sqrt x0) - (sqrt x3)) * ((sqrt x0) + (sqrt x3)))) / (((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))) * (x0 - x3))
by A3, SQUARE_1:35
.=
(((sqrt x0) - (sqrt x3)) * ((((sqrt x2) + (sqrt x1)) + (sqrt x0)) + (sqrt x3))) / (((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))) * (x0 - x3))
.=
(((sqrt x0) - (sqrt x3)) / (x0 - x3)) * (((((sqrt x2) + (sqrt x1)) + (sqrt x0)) + (sqrt x3)) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))
by XCMPLX_1:76
.=
(1 / ((sqrt x0) + (sqrt x3))) * (((((sqrt x2) + (sqrt x1)) + (sqrt x0)) + (sqrt x3)) / ((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))))
by A3, A6, SQUARE_1:36
.=
((((sqrt x2) + (sqrt x1)) + (sqrt x0)) + (sqrt x3)) / (((((((sqrt x2) + (sqrt x3)) * ((sqrt x3) + (sqrt x1))) * ((sqrt x0) + (sqrt x1))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x2) + (sqrt x0))) * ((sqrt x0) + (sqrt x3)))
by XCMPLX_1:103
.=
((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
;
hence
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
; verum