reconsider y = x mod p as Element of INT by INT_1:def 2;

A5: ( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ;

take s ; :: thesis: 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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

thus 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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A5; :: thesis: verum

now :: thesis: ex s being Element of INT st

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )end;

then consider s being Element of INT such that ( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

per cases
( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 )
;

end;

suppose A1:
(ALGO_EXGCD (p,y)) `3_3 = 1
; :: thesis: ex s being Element of INT st

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ; :: thesis: verum

end;

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

now :: thesis: ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )end;

hence
ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

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

end;

suppose A2:
(ALGO_EXGCD (p,y)) `2_3 < 0
; :: thesis: ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider z = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ;

reconsider s = p + z as Element of INT by INT_1:def 2;

ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ;

hence ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A2, A1; :: thesis: verum

end;reconsider s = p + z as Element of INT by INT_1:def 2;

ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ;

hence ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A2, A1; :: thesis: verum

suppose A3:
0 <= (ALGO_EXGCD (p,y)) `2_3
; :: thesis: ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider s = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ;

thus ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A3, A1; :: thesis: verum

end;thus ex s being Element of INT st

( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A3, A1; :: thesis: verum

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ; :: thesis: verum

suppose A4:
(ALGO_EXGCD (p,y)) `3_3 <> 1
; :: thesis: ex s being Element of INT st

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider s = {} as Element of INT by INT_1:def 2;

( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ;

hence ex s being Element of INT st

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A4; :: thesis: verum

end;( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ;

hence ex s being Element of INT st

( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A4; :: thesis: verum

A5: ( ( (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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ;

take s ; :: thesis: 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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

thus 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 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A5; :: thesis: verum