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:93;
(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:77
.=
((sqrt (a * b)) / c) + ((sqrt ((a * c) * (a * b))) / (b * c))
by SQUARE_1:97
.=
((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:97
.=
((sqrt (a * b)) / c) + (((sqrt (a ^2 )) * (sqrt (c * b))) / ((sqrt (b * c)) ^2 ))
by SQUARE_1:def 4
.=
((sqrt (a * b)) / c) + (((sqrt (a ^2 )) / (sqrt (b * c))) * ((sqrt (c * b)) / (sqrt (b * c))))
by XCMPLX_1:77
.=
((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:89
;
hence
(1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c)))
; verum