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
for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
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 for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
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: for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let i be Nat; :: thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume A2: B . i <> 0 ; :: thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
set k = (A . i) gcd (B . i);
A3: A . (i + 1) = B . i by A1;
A4: B . (i + 1) = (A . i) mod (B . i) by A1;
A5: (A . i) gcd (B . i) divides A . (i + 1) by A3, INT_2:def 2;
A6: (A . i) gcd (B . i) divides B . (i + 1)

proof

A7: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by A4, A2, INT_1:def 10;
A8: (A . i) gcd (B . i) divides A . i by INT_2:def 2;
(A . i) gcd (B . i) divides B . i by INT_2:def 2;
then consider s, t being Integer such that
A11: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by A7, A8;
B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by A11;
hence (A . i) gcd (B . i) divides B . (i + 1) ; :: thesis: verum

end;

for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds
m divides (A . i) gcd (B . i)

proof

let m be Integer; :: thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) )
assume A12: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; :: thesis: m divides (A . i) gcd (B . i)
then A13: m divides B . i by A1;
A14: m divides A . i

proof

B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by A4, A2, INT_1:def 10;
then A15: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ;
A16: ex s being Integer st B . i = m * s by A13;
A17: ex t being Integer st B . (i + 1) = m * t by A12;
consider s, t being Integer such that
A18: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by A15, A16, A17;
A . i = m * (s + (((A . i) div (B . i)) * t)) by A18;
hence m divides A . i ; :: thesis: verum

end;

thus m divides (A . i) gcd (B . i) by A13, A14, INT_2:def 2; :: thesis: verum

end;

hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by A5, A6, INT_2:def 2; :: thesis: verum