let p, i be Nat; :: thesis: ( p is prime & i mod p = - 1 implies (i ^2 ) mod p = 1 )
assume A1: ( p is prime & i mod p = - 1 ) ; :: thesis: (i ^2 ) mod p = 1
then A2: p > 1 by INT_2:def 5;
p <> 0 by A1, INT_2:def 5;
then i mod p = i - ((i div p) * p) by INT_1:def 8;
then i = ((i div p) * p) - 1 by A1;
then A3: i ^2 = (((((i div p) * p) - 2) * (i div p)) * p) + 1 ;
(i ^2 ) mod p = 1 mod p by A3, Th10
.= 1 by A2, NAT_D:24 ;
hence (i ^2 ) mod p = 1 ; :: thesis: verum