let a, b be Element of INT ; :: thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
let A, B be sequence of INT; :: thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT )
assume AS1: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
LMM: for x being set st x in { i where i is Element of NAT : B . i = 0 } holds
x in NAT

proof

let x be set ; :: thesis: ( x in { i where i is Element of NAT : B . i = 0 } implies x in NAT )
assume x in { i where i is Element of NAT : B . i = 0 } ; :: thesis: x in NAT
then ex i being Element of NAT st
( x = i & B . i = 0 ) ;
hence x in NAT ; :: thesis: verum

end;

ex m0 being Element of NAT st B . m0 = 0

proof

assume A20: for m0 being Element of NAT holds not B . m0 = 0 ; :: thesis: contradiction
A2: for m0 being Element of NAT holds abs (B . m0) <> 0

proof

let m0 be Element of NAT ; :: thesis: abs (B . m0) <> 0
B . m0 <> 0 by A20;
hence abs (B . m0) <> 0 by ABSVALUE:2; :: thesis: verum

end;

A3: for i being Element of NAT holds abs (B . (i + 1)) <= (abs (B . i)) - 1

proof

let i be Element of NAT ; :: thesis: abs (B . (i + 1)) <= (abs (B . i)) - 1
abs (B . (i + 1)) = abs ((A . i) mod (B . i)) by AS1;
then abs (B . (i + 1)) < abs (B . i) by A2, LM5G1;
then (abs (B . (i + 1))) + 1 <= abs (B . i) by NAT_1:13;
then ((abs (B . (i + 1))) + 1) - 1 <= (abs (B . i)) - 1 by XREAL_1:9;
hence abs (B . (i + 1)) <= (abs (B . i)) - 1 ; :: thesis: verum

end;

defpred S₁[ Nat] means abs (B . $1) <= (abs (B . 0)) - $1;
P0: S₁[ 0 ] ;
P1: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume P11: S₁[i] ; :: thesis: S₁[i + 1]
P12: abs (B . (i + 1)) <= (abs (B . i)) - 1 by A3;
(abs (B . i)) - 1 <= ((abs (B . 0)) - i) - 1 by P11, XREAL_1:9;
hence S₁[i + 1] by XXREAL_0:2, P12; :: thesis: verum

end;

A4: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(P0, P1);
abs (B . (abs (B . 0))) <= (abs (B . 0)) - (abs (B . 0)) by A4;
hence contradiction by A2, NAT_1:14; :: thesis: verum

end;

then consider m0 being Element of NAT such that
X1: B . m0 = 0 ;
m0 in { i where i is Element of NAT : B . i = 0 } by X1;
hence { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by LMM, TARSKI:def 3; :: thesis: verum