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 Element of NAT such that
P0: ( 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 Element of 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 Element of 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 defALGOEXGCD;

P2X: now :: thesis: for i being Element of NAT holds
( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) )

let i be Element of NAT ; :: thesis: ( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) )
thus g . (i + 1) = w . i by P0; :: thesis: w . (i + 1) = (g . i) mod (w . i)
thus w . (i + 1) = t . (i + 1) by P0
.= (g . i) mod (w . i) by P0 ; :: thesis: verum

end;

X0: { i where i is Element of NAT : w . i = 0 } is non empty Subset of NAT by P0, P2X, LM5G;
then istop in { i where i is Element of NAT : w . i = 0 } by P0, NAT_1:def 1;
then P4: ex i being Element of NAT st
( istop = i & w . i = 0 ) ;
XX3: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop)

proof

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

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

then abs (g . istop) = g . istop by ABSVALUE:def 1;
hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, MCART_1:def 7; :: thesis: verum

end;

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

then abs (g . istop) = - (g . istop) by ABSVALUE:def 1;
hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, XX32, MCART_1:def 7; :: thesis: verum

end;

end;

end;

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

suppose C1: 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 )

thus R1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P0, P4, LM6G, XX3, C1; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y :: thesis: verum

proof

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

suppose Y11: 0 <= g . istop ; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y

Y13: (ALGO_EXGCD (x,y)) `1_3 = 1 by C1, P0, Y11, MCART_1:def 5;
(ALGO_EXGCD (x,y)) `2_3 = 0 by C1, P0, MCART_1:def 6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y11, P0, C1, XX3, ABSVALUE:def 1, Y13, R1; :: thesis: verum

end;

suppose XX32: g . istop < 0 ; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y

Y13: (ALGO_EXGCD (x,y)) `1_3 = - 1 by C1, P0, XX32, MCART_1:def 5;
(ALGO_EXGCD (x,y)) `2_3 = 0 by P0, C1, MCART_1:def 6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by P0, C1, XX3, ABSVALUE:def 1, XX32, Y13, R1; :: thesis: verum

end;

end;

end;

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 <= istop by NAT_1:14;
then 1 - 1 <= istop - 1 by XREAL_1:9;
then reconsider m1 = istop - 1 as Element of NAT by INT_1:3;
X1: w . m1 <> 0

proof

assume w . m1 = 0 ; :: thesis: contradiction
then X11: m1 in { i where i is Element of NAT : w . i = 0 } ;
istop - 1 < istop - 0 by XREAL_1:15;
hence contradiction by X11, P0, X0, NAT_1:def 1; :: thesis: verum

end;

P5: (g . m1) gcd (w . m1) = (g . (m1 + 1)) gcd (w . (m1 + 1)) by LM3G, P0, X1, P2X;
R1: (g . istop) gcd (w . istop) = (ALGO_EXGCD (x,y)) `3_3 by XX3, LM6G, P4;
hence RR1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P5, X1, P2X, LM4G, P0; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
Y1: ((a . (m1 + 1)) * x) + ((b . (m1 + 1)) * y) = g . (m1 + 1) by X1, LM7G, P0;
thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y :: thesis: verum

proof

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

suppose Y11: 0 <= g . istop ; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y

then Y12: (ALGO_EXGCD (x,y)) `3_3 = g . istop by XX3, ABSVALUE:def 1;
(ALGO_EXGCD (x,y)) `1_3 = a . istop by P0, Y11, MCART_1:def 5;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by RR1, Y1, Y12, P0, MCART_1:def 6; :: thesis: verum

end;

suppose XX32: g . istop < 0 ; :: thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y

then Y12: (ALGO_EXGCD (x,y)) `3_3 = - (g . istop) by XX3, ABSVALUE:def 1;
Y13: (ALGO_EXGCD (x,y)) `1_3 = - (a . istop) by P0, XX32, MCART_1:def 5;
(ALGO_EXGCD (x,y)) `2_3 = - (b . istop) by P0, XX32, MCART_1:def 6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y1, Y12, Y13, R1, P5, X1, P2X, LM4G, P0; :: thesis: verum

end;

end;

end;

end;

end;