let x, y, p be Element of INT ; :: thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p )
assume A1: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 ) ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
A2: ( (ALGO_EXGCD (p,y)) `3_3 = p gcd y & (((ALGO_EXGCD (p,y)) `1_3) * p) + (((ALGO_EXGCD (p,y)) `2_3) * y) = p gcd y ) by Th6;
reconsider s1 = ((ALGO_EXGCD (p,y)) `1_3) * p as Integer ;
reconsider s2 = ((ALGO_EXGCD (p,y)) `2_3) * y as Integer ;
reconsider s3 = (ALGO_EXGCD (p,y)) `2_3 as Integer ;
A3: p mod p = 0 by INT_1:50;
A4: (((ALGO_EXGCD (p,y)) `1_3) * p) mod p = ((((ALGO_EXGCD (p,y)) `1_3) mod p) * (p mod p)) mod p by NAT_D:67
.= 0 by A3, INT_1:73 ;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
A5: ((((ALGO_EXGCD (p,y)) `1_3) * p) + (((ALGO_EXGCD (p,y)) `2_3) * y)) mod p = ((s1 mod p) + (s2 mod p)) mod p by NAT_D:66
.= (((ALGO_EXGCD (p,y)) `2_3) * y) mod p by Th1, A4 ;

per cases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ;

suppose (ALGO_EXGCD (p,y)) `2_3 < 0 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

then consider z being Element of INT such that
A6: ( z = (ALGO_EXGCD (p,y)) `2_3 & ALGO_INVERSE (x,p) = p + z ) by Def3, A1;
thus ((ALGO_INVERSE (x,p)) * x) mod p = ((p * x) + (z * x)) mod p by A6
.= (z * x) mod p by NAT_D:61
.= ((z mod p) * (x mod p)) mod p by NAT_D:67
.= ((z mod p) * ((x mod p) mod p)) mod p by Th1
.= 1 mod p by A5, A6, A2, A1, NAT_D:67 ; :: thesis: verum

end;

suppose 0 <= (ALGO_EXGCD (p,y)) `2_3 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

hence ((ALGO_INVERSE (x,p)) * x) mod p = (((ALGO_EXGCD (p,y)) `2_3) * x) mod p by Def3, A1
.= ((s3 mod p) * (x mod p)) mod p by NAT_D:67
.= ((s3 mod p) * ((x mod p) mod p)) mod p by Th1
.= 1 mod p by A5, A2, A1, NAT_D:67 ;
:: thesis: verum

end;

end;