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