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