let r be irrational Real; :: thesis: for a1, a2, b1, b2 being Element of REAL

for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

let a1, a2, b1, b2 be Element of REAL ; :: thesis: for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

let r1 be non negative Real; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 implies ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) )

assume A1: |.((a1 * b2) - (a2 * b1)).| <> 0 ; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

consider q being Element of RAT such that

A2: denominator q > [\r1/] + 1 and

A3: q in HWZSet r by Th42;

for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

let a1, a2, b1, b2 be Element of REAL ; :: thesis: for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

let r1 be non negative Real; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 implies ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) )

assume A1: |.((a1 * b2) - (a2 * b1)).| <> 0 ; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

consider q being Element of RAT such that

A2: denominator q > [\r1/] + 1 and

A3: q in HWZSet r by Th42;

per cases
( (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 or (a2 * (denominator q)) + (b2 * (numerator q)) = 0 )
;

end;

suppose
(a2 * (denominator q)) + (b2 * (numerator q)) <> 0
; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

hence
ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A2, A3; :: thesis: verum

end;( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A2, A3; :: thesis: verum

suppose A5:
(a2 * (denominator q)) + (b2 * (numerator q)) = 0
; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

consider q1 being Element of RAT such that

A6: denominator q1 > [\(denominator q)/] + 1 and

A7: q1 in HWZSet r by Th42;

denominator q1 > denominator q by A6, INT_1:29, XXREAL_0:2;

then A8: denominator q1 > [\r1/] + 1 by A2, XXREAL_0:2;

q1 <> q by A6, INT_1:29;

then (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 by A1, A5, Th43;

hence ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A7, A8; :: thesis: verum

end;A6: denominator q1 > [\(denominator q)/] + 1 and

A7: q1 in HWZSet r by Th42;

denominator q1 > denominator q by A6, INT_1:29, XXREAL_0:2;

then A8: denominator q1 > [\r1/] + 1 by A2, XXREAL_0:2;

q1 <> q by A6, INT_1:29;

then (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 by A1, A5, Th43;

hence ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A7, A8; :: thesis: verum