let b, c, a be real positive number ; :: 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