let x, y be Element of INT ; :: thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y )
consider g, w, q, t, a, b, v, u being sequence of INT, istop being Nat such that
A1: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Nat : w . i = 0 } & ( 0 <= g . istop implies ALGO_EXGCD (x,y) = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies ALGO_EXGCD (x,y) = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) by Def2;

A2: now :: thesis: for i being Nat holds
( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) )

let i be Nat; :: thesis: ( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) )
thus g . (i + 1) = w . i by A1; :: thesis: w . (i + 1) = (g . i) mod (w . i)
thus w . (i + 1) = t . (i + 1) by A1
.= (g . i) mod (w . i) by A1 ; :: thesis: verum

end;

A3: { i where i is Nat : w . i = 0 } is non empty Subset of NAT by A1, A2, Lm10;
then istop in { i where i is Nat : w . i = 0 } by A1, NAT_1:def 1;
then A4: ex i being Nat st
( istop = i & w . i = 0 ) ;
A5: (ALGO_EXGCD (x,y)) `3_3 = |.(g . istop).|

proof

per cases ( 0 <= g . istop or g . istop < 0 ) ;

suppose 0 <= g . istop ; :: thesis: (ALGO_EXGCD (x,y)) `3_3 = |.(g . istop).|

hence (ALGO_EXGCD (x,y)) `3_3 = |.(g . istop).| by A1, ABSVALUE:def 1; :: thesis: verum

end;

suppose g . istop < 0 ; :: thesis: (ALGO_EXGCD (x,y)) `3_3 = |.(g . istop).|

hence (ALGO_EXGCD (x,y)) `3_3 = |.(g . istop).| by A1, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

per cases ( istop = 0 or istop <> 0 ) ;

suppose A7: istop = 0 ; :: thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y )

hence (ALGO_EXGCD (x,y)) `3_3 = x gcd y by A1, A4, Lm11, A5; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by A1, A7; :: thesis: verum

end;

suppose istop <> 0 ; :: thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y )

then 1 - 1 <= istop - 1 by XREAL_1:9, NAT_1:14;
then reconsider m1 = istop - 1 as Element of NAT by INT_1:3;
A9: w . m1 <> 0

proof

assume w . m1 = 0 ; :: thesis: contradiction
then A10: m1 in { i where i is Nat : w . i = 0 } ;
istop - 1 < istop - 0 by XREAL_1:15;
hence contradiction by A10, A1, A3, NAT_1:def 1; :: thesis: verum

end;

A11: (g . m1) gcd (w . m1) = (g . (m1 + 1)) gcd (w . (m1 + 1)) by Lm8, A1, A9, A2;
(g . istop) gcd (w . istop) = (ALGO_EXGCD (x,y)) `3_3 by A5, Lm11, A4;
hence A13: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by A11, A9, A2, Lm9, A1; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
((a . (m1 + 1)) * x) + ((b . (m1 + 1)) * y) = g . (m1 + 1) by A9, Lm12, A1;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by A13, A1; :: thesis: verum

end;

end;