let b, c, a be real positive number ; :: thesis: ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2 ) + (((a * b) / c) ^2 )) + (((b * c) / a) ^2 )) + (2 * (((a ^2 ) + (b ^2 )) + (c ^2 )))
((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((b * c) / a) ^2 ) + (((c * a) / b) ^2 )) + (((a * b) / c) ^2 )) + ((((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)))
.= (((((b * c) / a) ^2 ) + (((c * a) / b) ^2 )) + (((a * b) / c) ^2 )) + (2 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) by Lm15 ;
hence ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2 ) + (((a * b) / c) ^2 )) + (((b * c) / a) ^2 )) + (2 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) ; :: thesis: verum