let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies for n being Nat st n > a * b holds
ex x, y being non zero Nat st n = (a * x) + (b * y) )
assume A1: a,b are_coprime ; :: thesis: for n being Nat st n > a * b holds
ex x, y being non zero Nat st n = (a * x) + (b * y)
let n be Nat; :: thesis: ( n > a * b implies ex x, y being non zero Nat st n = (a * x) + (b * y) )
assume A3: n > a * b ; :: thesis: ex x, y being non zero Nat st n = (a * x) + (b * y)
consider u, v being Nat such that
A2: (a * u) - (b * v) = 1 by A1, SierpTh16;
A5: n = n * ((a * u) - (b * v)) by A2
.= ((a * n) * u) - ((b * n) * v) ;
then (a * b) / (a * b) < (((a * n) * u) - ((b * n) * v)) / (a * b) by A3, XREAL_1:74;
then 1 < (((a * n) * u) / (a * b)) - (((b * n) * v) / (a * b)) by XCMPLX_1:60;
then 1 < ((((n * u) * a) / a) / b) - (((b * n) * v) / (a * b)) by XCMPLX_1:78;
then 1 < ((n * u) / b) - (((b * n) * v) / (a * b)) by XCMPLX_1:89;
then 1 < ((n * u) / b) - ((((n * v) * b) / b) / a) by XCMPLX_1:78;
then 1 < ((n * u) / b) - ((n * v) / a) by XCMPLX_1:89;
then consider t being Integer such that
B1: ( (n * u) / b > t & t > (n * v) / a ) by Cosik1;
set x = (n * u) - (b * t);
set y = (a * t) - (n * v);
((n * u) / b) * b > t * b by B1, XREAL_1:68;
then n * u > (t * b) + 0 by XCMPLX_1:87;
then T1: (n * u) - (b * t) > 0 by XREAL_1:20;
t * a > ((n * v) / a) * a by B1, XREAL_1:68;
then t * a > (n * v) + 0 by XCMPLX_1:87;
then T2: (a * t) - (n * v) > 0 by XREAL_1:20;
(a * ((n * u) - (b * t))) + (b * ((a * t) - (n * v))) = n by A5;
hence ex x, y being non zero Nat st n = (a * x) + (b * y) by T1, T2; :: thesis: verum