let b, a be real number ; :: thesis: ( 0 <= b & b < a implies 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b) )
assume A1: ( 0 <= b & b < a ) ; :: thesis: 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)
hence 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (((sqrt a) ^2 ) - ((sqrt b) ^2 )) by Lm6, Th70
.= ((sqrt a) - (sqrt b)) / (a - ((sqrt b) ^2 )) by A1, Def4
.= ((sqrt a) - (sqrt b)) / (a - b) by A1, Def4 ;
:: thesis: verum