let a, b be Integer; :: thesis: ALGO_GCD (a,b) = a gcd b

consider A, B being sequence of NAT such that

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) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Nat : B . i = 0 } ) ) by Def1;

set m0 = min* { i where i is Nat : B . i = 0 } ;

A2: { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A1, Lm5;

then min* { i where i is Nat : B . i = 0 } in { i where i is Nat : B . i = 0 } by NAT_1:def 1;

then A3: ex i being Nat st

( min* { i where i is Nat : B . i = 0 } = i & B . i = 0 ) ;

consider A, B being sequence of NAT such that

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) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Nat : B . i = 0 } ) ) by Def1;

set m0 = min* { i where i is Nat : B . i = 0 } ;

A2: { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A1, Lm5;

then min* { i where i is Nat : B . i = 0 } in { i where i is Nat : B . i = 0 } by NAT_1:def 1;

then A3: ex i being Nat st

( min* { i where i is Nat : B . i = 0 } = i & B . i = 0 ) ;

per cases
( min* { i where i is Nat : B . i = 0 } = 0 or min* { i where i is Nat : B . i = 0 } <> 0 )
;

end;

suppose
min* { i where i is Nat : B . i = 0 } = 0
; :: thesis: ALGO_GCD (a,b) = a gcd b

hence ALGO_GCD (a,b) =
(A . 0) gcd (B . 0)
by A3, NEWTON:52, A1

.= a gcd b by A1, INT_2:34 ;

:: thesis: verum

end;.= a gcd b by A1, INT_2:34 ;

:: thesis: verum

suppose
min* { i where i is Nat : B . i = 0 } <> 0
; :: thesis: ALGO_GCD (a,b) = a gcd b

then
1 - 1 <= (min* { i where i is Nat : B . i = 0 } ) - 1
by XREAL_1:9, NAT_1:14;

then reconsider m1 = (min* { i where i is Nat : B . i = 0 } ) - 1 as Element of NAT by INT_1:3;

A5: B . m1 <> 0

A8: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by Lm3, A5, A1;

(A . (min* { i where i is Nat : B . i = 0 } )) gcd (B . (min* { i where i is Nat : B . i = 0 } )) = ALGO_GCD (a,b) by A1, NEWTON:52, A3;

hence ALGO_GCD (a,b) = a gcd b by A8, A7, A1, INT_2:34; :: thesis: verum

end;then reconsider m1 = (min* { i where i is Nat : B . i = 0 } ) - 1 as Element of NAT by INT_1:3;

A5: B . m1 <> 0

proof

then A7:
(A . 0) gcd (B . 0) = (A . m1) gcd (B . m1)
by A1, Lm4;
assume
B . m1 = 0
; :: thesis: contradiction

then A6: m1 in { i where i is Nat : B . i = 0 } ;

(min* { i where i is Nat : B . i = 0 } ) - 1 < (min* { i where i is Nat : B . i = 0 } ) - 0 by XREAL_1:15;

hence contradiction by A6, A2, NAT_1:def 1; :: thesis: verum

end;then A6: m1 in { i where i is Nat : B . i = 0 } ;

(min* { i where i is Nat : B . i = 0 } ) - 1 < (min* { i where i is Nat : B . i = 0 } ) - 0 by XREAL_1:15;

hence contradiction by A6, A2, NAT_1:def 1; :: thesis: verum

A8: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by Lm3, A5, A1;

(A . (min* { i where i is Nat : B . i = 0 } )) gcd (B . (min* { i where i is Nat : B . i = 0 } )) = ALGO_GCD (a,b) by A1, NEWTON:52, A3;

hence ALGO_GCD (a,b) = a gcd b by A8, A7, A1, INT_2:34; :: thesis: verum