let k, x0, x1, x2 be Real; for f being Function of REAL ,REAL st ( for x being Real holds f . x = k / (x ^2 ) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))
let f be Function of REAL ,REAL ; ( ( for x being Real holds f . x = k / (x ^2 ) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2)) )
assume that
A1:
for x being Real holds f . x = k / (x ^2 )
and
A2:
( x0 <> 0 & x1 <> 0 & x2 <> 0 )
and
A3:
x0,x1,x2 are_mutually_different
; [!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))
A4:
( f . x0 = k / (x0 ^2 ) & f . x1 = k / (x1 ^2 ) & f . x2 = k / (x2 ^2 ) )
by A1;
A5:
( x1 - x0 <> 0 & x2 - x1 <> 0 & x0 - x2 <> 0 )
by A3, ZFMISC_1:def 5;
[!f,x0,x1,x2!] =
(((k * ((1 / (x0 ^2 )) - (1 / (x1 ^2 )))) / (x0 - x1)) - ((k * ((1 / (x1 ^2 )) - (1 / (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)
by A4
.=
(((k * (((1 * (x1 ^2 )) - (1 * (x0 ^2 ))) / ((x0 ^2 ) * (x1 ^2 )))) / (x0 - x1)) - ((k * ((1 / (x1 ^2 )) - (1 / (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)
by A2, XCMPLX_1:131
.=
(((k * (((1 * (x1 ^2 )) - (1 * (x0 ^2 ))) / ((x0 ^2 ) * (x1 ^2 )))) / (x0 - x1)) - ((k * (((1 * (x2 ^2 )) - (1 * (x1 ^2 ))) / ((x1 ^2 ) * (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)
by A2, XCMPLX_1:131
.=
((k * ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (- (x1 - x0)))) - (k * ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / (- (x2 - x1))))) / (x0 - x2)
.=
((k * (- ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (x1 - x0)))) - (k * ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / (- (x2 - x1))))) / (x0 - x2)
by XCMPLX_1:189
.=
((- (k * ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (x1 - x0)))) - (k * (- ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / (x2 - x1))))) / (x0 - x2)
by XCMPLX_1:189
.=
((- (k * ((((x1 - x0) * (x1 + x0)) / (x1 - x0)) / ((x0 ^2 ) * (x1 ^2 ))))) + (k * ((((x2 - x1) * (x2 + x1)) / (x2 - x1)) / ((x1 ^2 ) * (x2 ^2 ))))) / (x0 - x2)
.=
((- (k * ((x1 + x0) / ((x0 ^2 ) * (x1 ^2 ))))) + (k * ((((x2 - x1) * (x2 + x1)) / (x2 - x1)) / ((x1 ^2 ) * (x2 ^2 ))))) / (x0 - x2)
by A5, XCMPLX_1:90
.=
((- (k * ((x1 / (((x0 * x0) * x1) * x1)) + (x0 / (((x0 * x0) * x1) * x1))))) + (k * ((x2 + x1) / (((x1 * x1) * x2) * x2)))) / (x0 - x2)
by A5, XCMPLX_1:90
.=
((- (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + (x0 / (x0 * ((x0 * x1) * x1)))))) + (k * ((x2 / (x2 * ((x1 * x1) * x2))) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)
by XCMPLX_1:104
.=
((- (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + (x0 / (x0 * ((x0 * x1) * x1)))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)
by XCMPLX_1:104
.=
((- (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)
by XCMPLX_1:104
.=
((- (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)
by XCMPLX_1:104
.=
((- (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)
by A2, XCMPLX_1:60
.=
((- (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * 1) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)
by A2, XCMPLX_1:60
.=
((- (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * 1)))) + (k * (((1 / ((x1 * x1) * x2)) * 1) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)
by A2, XCMPLX_1:60
.=
((- (k * ((1 / (x0 * (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * ((1 / (x1 * (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)
by A2, XCMPLX_1:60
.=
((- (k * (((1 / x0) * (1 / (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * ((1 / (x1 * (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)
by XCMPLX_1:103
.=
((- (k * (((1 / x0) * (1 / (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * (((1 / x1) * (1 / (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)
by XCMPLX_1:103
.=
((- (k * (((1 / x0) * (1 / (x0 * x1))) + ((1 / (x0 * x1)) * (1 / x1))))) + (k * (((1 / x1) * (1 / (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)
by XCMPLX_1:103
.=
((- ((k * (1 / (x0 * x1))) * ((1 / x0) + (1 / x1)))) + (k * (((1 / x1) * (1 / (x1 * x2))) + ((1 / (x1 * x2)) * (1 / x2))))) / (x0 - x2)
by XCMPLX_1:103
.=
k * ((((1 / (x1 * x2)) / (x0 - x2)) * ((1 / x1) + (1 / x2))) - (((1 / (x0 * x1)) / (x0 - x2)) * ((1 / x0) + (1 / x1))))
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) * ((1 / x1) + (1 / x2))) - (((1 / (x0 * x1)) / (x0 - x2)) * ((1 / x0) + (1 / x1))))
by XCMPLX_1:79
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) * ((1 / x1) + (1 / x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((1 / x0) + (1 / x1))))
by XCMPLX_1:79
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) * (((1 * x2) + (1 * x1)) / (x1 * x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((1 / x0) + (1 / x1))))
by A2, XCMPLX_1:117
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) * (((1 * x2) + (1 * x1)) / (x1 * x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * (((1 * x1) + (1 * x0)) / (x0 * x1))))
by A2, XCMPLX_1:117
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((x1 + x0) / (x0 * x1))))
by XCMPLX_1:80
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))
by XCMPLX_1:80
.=
k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))
by XCMPLX_1:83
.=
k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - (((1 / ((x0 * x1) * (x0 - x2))) / (x0 * x1)) * (x1 + x0)))
by XCMPLX_1:83
.=
k * ((((x2 + x1) / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) - (((x1 + x0) / ((x0 * x1) * (x0 - x2))) / (x0 * x1)))
.=
k * (((x2 + x1) / (((x1 * x2) * (x0 - x2)) * (x1 * x2))) - (((x1 + x0) / ((x0 * x1) * (x0 - x2))) / (x0 * x1)))
by XCMPLX_1:79
.=
k * (((x2 + x1) / (((x1 * x2) * (x0 - x2)) * (x1 * x2))) - ((x1 + x0) / (((x0 * x1) * (x0 - x2)) * (x0 * x1))))
by XCMPLX_1:79
.=
k * (((x2 + x1) / (((x1 ^2 ) * (x0 - x2)) * (x2 ^2 ))) - ((x1 + x0) / (((x1 ^2 ) * (x0 - x2)) * (x0 ^2 ))))
.=
k * ((((x2 + x1) / ((x1 ^2 ) * (x0 - x2))) / (x2 ^2 )) - ((x1 + x0) / (((x1 ^2 ) * (x0 - x2)) * (x0 ^2 ))))
by XCMPLX_1:79
.=
k * (((1 / ((x1 ^2 ) * (x0 - x2))) * ((x2 + x1) / (x2 ^2 ))) - (((x1 + x0) / ((x1 ^2 ) * (x0 - x2))) / (x0 ^2 )))
by XCMPLX_1:79
.=
k * ((1 / ((x1 ^2 ) * (x0 - x2))) * (((x2 + x1) / (x2 ^2 )) - ((x1 + x0) / (x0 ^2 ))))
.=
k * ((1 / ((x1 ^2 ) * (x0 - x2))) * ((((x2 + x1) * (x0 ^2 )) - ((x1 + x0) * (x2 ^2 ))) / ((x2 ^2 ) * (x0 ^2 ))))
by A2, XCMPLX_1:131
.=
k * ((((1 * (x0 - x2)) / ((x1 ^2 ) * (x0 - x2))) * ((x1 * (x0 + x2)) + (x0 * x2))) / ((x2 ^2 ) * (x0 ^2 )))
.=
k * (((1 / (x1 ^2 )) * (((x1 * x0) + (x1 * x2)) + (x0 * x2))) / ((x2 ^2 ) * (x0 ^2 )))
by A5, XCMPLX_1:92
.=
k * (((((x1 * x0) + (x1 * x2)) + (x0 * x2)) / (x1 ^2 )) / ((x2 ^2 ) * (x0 ^2 )))
.=
k * ((((x1 * x0) + (x1 * x2)) + (x0 * x2)) / ((x1 ^2 ) * ((x2 ^2 ) * (x0 ^2 ))))
by XCMPLX_1:79
.=
k * ((((1 * (x1 * x0)) / (((x1 * (x2 ^2 )) * x0) * (x1 * x0))) + ((1 * (x1 * x2)) / (((x1 * x2) * (x0 ^2 )) * (x1 * x2)))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2))))
.=
k * (((1 / ((x1 * (x2 ^2 )) * x0)) + ((1 * (x1 * x2)) / (((x1 * x2) * (x0 ^2 )) * (x1 * x2)))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2))))
by A2, XCMPLX_1:92
.=
k * (((1 / ((x1 * (x2 ^2 )) * x0)) + (1 / ((x1 * x2) * (x0 ^2 )))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2))))
by A2, XCMPLX_1:92
.=
k * (((1 / (((x1 * x2) * x0) * x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))
by A2, XCMPLX_1:92
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))
by XCMPLX_1:103
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + (1 / (((x1 * x2) * x0) * x1)))
by XCMPLX_1:103
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + ((1 / ((x1 * x2) * x0)) * (1 / x1)))
by XCMPLX_1:103
.=
(k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))
;
hence
[!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))
; verum