:: deftheorem Def3 defines ALGO_INVERSE NTALGO_1:def 3 :
for x, p, b₃ being Element of INT holds
( b₃ = ALGO_INVERSE (x,p) iff for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & b<sub>3</sub> = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b₃ = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b₃ = {} ) ) );