let a1, a2, b1, b2 be Element of REAL ; :: thesis: for q, q1 being Element of RAT st |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 holds
(a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
let q, q1 be Element of RAT ; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 implies (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 )
assume that
A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and
A2: q <> q1 and
A3: (a2 * (denominator q)) + (b2 * (numerator q)) = 0 ; :: thesis: (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
A5: (- a2) * (denominator q) = (numerator q) * b2 by A3;
per cases ( ( a2 <> 0 & b2 <> 0 ) or ( a2 <> 0 & b2 = 0 ) or ( a2 = 0 & b2 <> 0 ) ) by A1;
suppose A4: ( a2 <> 0 & b2 <> 0 ) ; :: thesis: (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
assume (a2 * (denominator q1)) + (b2 * (numerator q1)) = 0 ; :: thesis: contradiction
then A7: (- a2) * (denominator q1) = b2 * (numerator q1) ;
q = (numerator q) / (denominator q) by RAT_1:15
.= (- a2) / b2 by A4, A5, XCMPLX_1:94
.= (numerator q1) / (denominator q1) by A4, A7, XCMPLX_1:94
.= q1 by RAT_1:15 ;
hence contradiction by A2; :: thesis: verum
end;
suppose ( a2 <> 0 & b2 = 0 ) ; :: thesis: (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
hence (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 ; :: thesis: verum
end;
suppose A10: ( a2 = 0 & b2 <> 0 ) ; :: thesis: (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0
assume A11: (a2 * (denominator q1)) + (b2 * (numerator q1)) = 0 ; :: thesis: contradiction
q = 0 by A3, A10
.= q1 by A10, A11 ;
hence contradiction by A2; :: thesis: verum
end;
end;