let a, b be Real; :: thesis: ( a <> 0 & b ^2 = 1 + (a * a) implies (((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1 )
assume that
A1: a <> 0 and
A2: b ^2 = 1 + (a * a) ; :: thesis: (((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1
A3: b <> 0
proof
assume b = 0 ; :: thesis: contradiction
then a ^2 = - 1 by A2;
hence contradiction by A1, SQUARE_1:12; :: thesis: verum
end;
(((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = ((1 / b) * (((- 1) * 1) / b)) * ((a * a) + 1)
.= ((1 / b) * ((- 1) * (1 / b))) * ((a * a) + 1) by XCMPLX_1:74
.= (- 1) * (((1 / b) ^2) * (b ^2)) by A2
.= (- 1) * 1 by A3, Lem05 ;
hence (((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1 ; :: thesis: verum