let x, p, y be Element of INT ; :: thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p )
assume AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 ) ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

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

suppose C1: p = 0 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

thus ((ALGO_INVERSE (x,p)) * x) mod p = 0 by C1, INT_1:def 10
.= 1 mod p by C1, INT_1:def 10 ; :: thesis: verum

end;

suppose p <> 0 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

hence ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p by LMTh30, AS; :: thesis: verum

end;

end;