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 ;
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 ) ;
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
.= a gcd b by ;
:: thesis: verum
end;
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 ;
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
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 A7: (A . 0) gcd (B . 0) = (A . m1) gcd (B . m1) by ;
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 ;
hence ALGO_GCD (a,b) = a gcd b by ; :: thesis: verum
end;
end;