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_distinct 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_distinct 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_distinct
; [!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:130
.=
(((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:130
.=
((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:188
.=
((- (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:188
.=
((- (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:89
.=
((- (k * ((x1 / (((x0 * x0) * x1) * x1)) + (x0 / (((x0 * x0) * x1) * x1))))) + (k * ((x2 + x1) / (((x1 * x1) * x2) * x2)))) / (x0 - x2)
by A5, XCMPLX_1:89
.=
((- (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:103
.=
((- (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:103
.=
((- (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:103
.=
((- (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:103
.=
((- (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:102
.=
((- (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:102
.=
((- (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:102
.=
((- ((k * (1 / (x0 * x1))) * ((1 / x0) + (1 / x1)))) + (k * (((1 / x1) * (1 / (x1 * x2))) + ((1 / (x1 * x2)) * (1 / x2))))) / (x0 - x2)
by XCMPLX_1:102
.=
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:78
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) * ((1 / x1) + (1 / x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((1 / x0) + (1 / x1))))
by XCMPLX_1:78
.=
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:116
.=
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:116
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((x1 + x0) / (x0 * x1))))
by XCMPLX_1:79
.=
k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))
by XCMPLX_1:79
.=
k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))
by XCMPLX_1:82
.=
k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - (((1 / ((x0 * x1) * (x0 - x2))) / (x0 * x1)) * (x1 + x0)))
by XCMPLX_1:82
.=
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:78
.=
k * (((x2 + x1) / (((x1 * x2) * (x0 - x2)) * (x1 * x2))) - ((x1 + x0) / (((x0 * x1) * (x0 - x2)) * (x0 * x1))))
by XCMPLX_1:78
.=
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:78
.=
k * (((1 / ((x1 ^2) * (x0 - x2))) * ((x2 + x1) / (x2 ^2))) - (((x1 + x0) / ((x1 ^2) * (x0 - x2))) / (x0 ^2)))
by XCMPLX_1:78
.=
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:130
.=
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:91
.=
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:78
.=
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:91
.=
k * (((1 / ((x1 * (x2 ^2)) * x0)) + (1 / ((x1 * x2) * (x0 ^2)))) + ((1 * (x0 * x2)) / ((((x1 ^2) * x2) * x0) * (x0 * x2))))
by A2, XCMPLX_1:91
.=
k * (((1 / (((x1 * x2) * x0) * x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))
by A2, XCMPLX_1:91
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))
by XCMPLX_1:102
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + (1 / (((x1 * x2) * x0) * x1)))
by XCMPLX_1:102
.=
k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + ((1 / ((x1 * x2) * x0)) * (1 / x1)))
by XCMPLX_1:102
.=
(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