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 Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is 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 Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Nat : B . i = 0 } is non empty Subset of NAT )

assume A1: ( A . 0 = a & B . 0 = b & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: { i where i is Nat : B . i = 0 } is non empty Subset of NAT

A2: for x being object st x in { i where i is Nat : B . i = 0 } holds

x in NAT

A11: B . m0 = 0 ;

m0 in { i where i is Nat : B . i = 0 } by A11;

hence { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A2, TARSKI:def 3; :: thesis: verum

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds

{ i where i is 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 Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Nat : B . i = 0 } is non empty Subset of NAT )

assume A1: ( A . 0 = a & B . 0 = b & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; :: thesis: { i where i is Nat : B . i = 0 } is non empty Subset of NAT

A2: for x being object st x in { i where i is Nat : B . i = 0 } holds

x in NAT

proof

ex m0 being Nat st B . m0 = 0
let x be object ; :: thesis: ( x in { i where i is Nat : B . i = 0 } implies x in NAT )

assume x in { i where i is Nat : B . i = 0 } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & B . i = 0 ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume x in { i where i is Nat : B . i = 0 } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & B . i = 0 ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

proof

then consider m0 being Nat such that
assume A3:
for m0 being Nat holds not B . m0 = 0
; :: thesis: contradiction

A4: for m0 being Nat holds |.(B . m0).| <> 0 by A3, ABSVALUE:2;

A5: for i being Nat holds |.(B . (i + 1)).| <= |.(B . i).| - 1_{1}[ Nat] means |.(B . $1).| <= |.(B . 0).| - $1;

A6: S_{1}[ 0 ]
;

A7: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A6, A7);

|.(B . |.(B . 0).|).| <= |.(B . 0).| - |.(B . 0).| by A10;

hence contradiction by A4, NAT_1:14; :: thesis: verum

end;A4: for m0 being Nat holds |.(B . m0).| <> 0 by A3, ABSVALUE:2;

A5: for i being Nat holds |.(B . (i + 1)).| <= |.(B . i).| - 1

proof

defpred S
let i be Nat; :: thesis: |.(B . (i + 1)).| <= |.(B . i).| - 1

|.(B . (i + 1)).| = |.((A . i) mod (B . i)).| by A1;

then |.(B . (i + 1)).| < |.(B . i).| by A4, Th5;

then |.(B . (i + 1)).| + 1 <= |.(B . i).| by NAT_1:13;

then (|.(B . (i + 1)).| + 1) - 1 <= |.(B . i).| - 1 by XREAL_1:9;

hence |.(B . (i + 1)).| <= |.(B . i).| - 1 ; :: thesis: verum

end;|.(B . (i + 1)).| = |.((A . i) mod (B . i)).| by A1;

then |.(B . (i + 1)).| < |.(B . i).| by A4, Th5;

then |.(B . (i + 1)).| + 1 <= |.(B . i).| by NAT_1:13;

then (|.(B . (i + 1)).| + 1) - 1 <= |.(B . i).| - 1 by XREAL_1:9;

hence |.(B . (i + 1)).| <= |.(B . i).| - 1 ; :: thesis: verum

A6: S

A7: for i being Nat st S

S

proof

A10:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A8: S_{1}[i]
; :: thesis: S_{1}[i + 1]

A9: |.(B . (i + 1)).| <= |.(B . i).| - 1 by A5;

|.(B . i).| - 1 <= (|.(B . 0).| - i) - 1 by A8, XREAL_1:9;

hence S_{1}[i + 1]
by A9, XXREAL_0:2; :: thesis: verum

end;assume A8: S

A9: |.(B . (i + 1)).| <= |.(B . i).| - 1 by A5;

|.(B . i).| - 1 <= (|.(B . 0).| - i) - 1 by A8, XREAL_1:9;

hence S

|.(B . |.(B . 0).|).| <= |.(B . 0).| - |.(B . 0).| by A10;

hence contradiction by A4, NAT_1:14; :: thesis: verum

A11: B . m0 = 0 ;

m0 in { i where i is Nat : B . i = 0 } by A11;

hence { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A2, TARSKI:def 3; :: thesis: verum