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
for i being Element of 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 Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS: ( 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: for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let i be Element of NAT ; :: thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS1: B . i <> 0 ; :: thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
set k = (A . i) gcd (B . i);
Q1: A . (i + 1) = B . i by AS;
Q2: B . (i + 1) = (A . i) mod (B . i) by AS;
P1: (A . i) gcd (B . i) divides A . (i + 1) by Q1, INT_2:def 2;
P2: (A . i) gcd (B . i) divides B . (i + 1)

proof

X1: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def 10, Q2, AS1;
X2: (A . i) gcd (B . i) divides A . i by INT_2:def 2;
X3: (A . i) gcd (B . i) divides B . i by INT_2:def 2;
X4: ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by X2, INT_1:def 3;
ex t being Integer st B . i = ((A . i) gcd (B . i)) * t by X3, INT_1:def 3;
then consider s, t being Integer such that
X5: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by X1, X4;
B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by X5;
hence (A . i) gcd (B . i) divides B . (i + 1) by INT_1:def 3; :: 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 P3: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; :: thesis: m divides (A . i) gcd (B . i)
then P31: m divides B . i by AS;
P32: m divides A . i

proof

B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def 10, Q2, AS1;
then X1: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ;
X21: ex s being Integer st B . i = m * s by INT_1:def 3, P31;
X22: ex t being Integer st B . (i + 1) = m * t by INT_1:def 3, P3;
consider s, t being Integer such that
X4: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by X1, X21, X22;
A . i = m * (s + (((A . i) div (B . i)) * t)) by X4;
hence m divides A . i by INT_1:def 3; :: thesis: verum

end;

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

end;

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