let f be Function of Gauss_INT_Ring,NAT; :: thesis: ( ( for x being G_INTEG holds f . x = Norm x ) implies for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring holds
ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) ) )
assume A1: for x being G_INTEG holds f . x = Norm x ; :: thesis: for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring holds
ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) )
let a, b be Element of Gauss_INT_Ring; :: thesis: ( b <> 0. Gauss_INT_Ring implies ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) ) )
assume A2: b <> 0. Gauss_INT_Ring ; :: thesis: ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) )
reconsider a0 = a, b0 = b as G_INTEG by Th2;
reconsider x = a0 / b0, b1 = b0 as G_RAT ;
consider m being Element of INT such that
A3: |.((Re x) - m).| <= 1 / 2 by Th48;
consider n being Element of INT such that
A4: |.((Im x) - n).| <= 1 / 2 by Th48;
set q0 = m + (n * <i>);
reconsider q0 = m + (n * <i>) as G_INTEG ;
reconsider q1 = q0 as G_RAT ;
reconsider r0 = a0 - (q0 * b0) as G_INTEG ;
A5: Re (x - q0) = (Re x) - (Re q0) by COMPLEX1:19
.= (Re x) - m by COMPLEX1:12 ;
A6: Im (x - q0) = (Im x) - (Im q0) by COMPLEX1:19
.= (Im x) - n by COMPLEX1:12 ;
reconsider xq1 = x - q1 as G_RAT ;
0 <= |.((Re x) - m).| by COMPLEX1:46;
then A7: |.((Re x) - m).| ^2 <= (1 / 2) ^2 by A3, SQUARE_1:15;
0 <= |.((Im x) - n).| by COMPLEX1:46;
then A8: |.((Im x) - n).| ^2 <= (1 / 2) ^2 by A4, SQUARE_1:15;
(|.((Re x) - m).| ^2) + (|.((Im x) - n).| ^2) <= ((1 / 2) ^2) + ((1 / 2) ^2) by A7, A8, XREAL_1:7;
then A9: Norm xq1 <= 1 / 2 by A5, A6, Th47;
reconsider bxq1 = b1 * xq1 as G_RAT ;
A10: b1 * xq1 = (b0 * (a0 / b0)) - (b0 * q0)
.= r0 by A2, XCMPLX_1:87 ;
A11: Norm bxq1 = (Norm b1) * (Norm xq1) by Th34;
A12: Norm r0 <= (Norm b1) / 2 by A9, A10, A11, XREAL_1:64;
Norm b0 <> 0 by A2, Th36;
then (Norm b1) / 2 < Norm b1 by XREAL_1:216;
then A13: Norm r0 < Norm b1 by A12, XXREAL_0:2;
reconsider q = q0, r = r0 as Element of Gauss_INT_Ring by Th3;
A14: q * b = q0 * b0 by Th6;
a0 = (q0 * b0) + r0 ;
then A15: a = (q * b) + r by A14, Th4;
A16: f . r = Norm r0 by A1;
f . b = Norm b0 by A1;
hence ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) ) by A13, A15, A16; :: thesis: verum