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