let a, b, c be positive Real; (((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))
; verum