let a be prime Nat; :: thesis: for b, c being rational number holds
( ((sqrt a) + b) * ((sqrt a) + c) is rational iff b = - c )
let b, c be rational number ; :: thesis: ( ((sqrt a) + b) * ((sqrt a) + c) is rational iff b = - c )
((sqrt a) + b) * ((sqrt a) + c) = ((((sqrt a) * (sqrt a)) + ((sqrt a) * c)) + ((sqrt a) * b)) + (b * c)
.= (a + (b * c)) + ((sqrt a) * (c + b)) ;
then ( ((sqrt a) + b) * ((sqrt a) + c) is rational iff b + c = 0 ) ;
hence ( ((sqrt a) + b) * ((sqrt a) + c) is rational iff b = - c ) ; :: thesis: verum