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 AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 ) ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
P3P: ( (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 Th2;
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 ;
P40C2: p mod p = 0 by INT_1:50;
P4: (((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 INT_4:12, P40C2 ;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
P6: ((((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 LMTh3, P4 ;

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
A11: ( z = (ALGO_EXGCD (p,y)) `2_3 & ALGO_INVERSE (x,p) = p + z ) by definverse, AS;
thus ((ALGO_INVERSE (x,p)) * x) mod p = ((p * x) + (z * x)) mod p by A11
.= (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 LMTh3
.= 1 mod p by P6, A11, P3P, AS, 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 definverse, AS
.= ((s3 mod p) * (x mod p)) mod p by NAT_D:67
.= ((s3 mod p) * ((x mod p) mod p)) mod p by LMTh3
.= 1 mod p by P6, P3P, AS, NAT_D:67 ;
:: thesis: verum

end;

end;