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