let a, b, c be positive Real; ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)
A1:
sqrt (b * a) > 0
by SQUARE_1:25;
((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) =
((((1 * 1) + (1 * ((sqrt (a * c)) / b))) + (((sqrt (b * c)) / a) * 1)) + (((sqrt (b * c)) / a) * ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c))
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * c)) * (sqrt (a * c))) / (a * b))) * (1 + ((sqrt (a * b)) / c))
by XCMPLX_1:76
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + ((sqrt ((b * c) * (a * c))) / (a * b))) * (1 + ((sqrt (a * b)) / c))
by SQUARE_1:29
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + ((sqrt ((b * a) * (c ^2))) / (a * b))) * (1 + ((sqrt (a * b)) / c))
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * (sqrt (c ^2))) / (a * b))) * (1 + ((sqrt (a * b)) / c))
by SQUARE_1:29
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * c) / (a * b))) * (1 + ((sqrt (a * b)) / c))
by SQUARE_1:22
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * c) / ((sqrt (a * b)) ^2))) * (1 + ((sqrt (a * b)) / c))
by SQUARE_1:def 2
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) / (sqrt (b * a))) * (c / (sqrt (b * a))))) * (1 + ((sqrt (a * b)) / c))
by XCMPLX_1:76
.=
(((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (1 * (c / (sqrt (b * a))))) * (1 + ((sqrt (a * b)) / c))
by A1, XCMPLX_1:60
.=
((((1 + ((sqrt (a * c)) / b)) + ((1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c))
.=
((((1 + ((sqrt (a * c)) / b)) + (((sqrt (a * b)) / c) + (a / (sqrt (b * c))))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c))
by Lm20
.=
(((((1 + ((sqrt (a * c)) / b)) + ((sqrt (a * b)) / c)) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((b / (sqrt (a * c))) + 1)
by Lm21
.=
(((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)
;
hence
((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)
; verum