let i be Nat; :: thesis: ( i <> 0 implies (i ^2) mod (i + 1) = 1 )
assume A1: i <> 0 ; :: thesis: (i ^2) mod (i + 1) = 1
then A2: i + 1 > 0 + 1 by XREAL_1:6;
i >= 1 by A1, NAT_1:14;
then i - 1 >= 1 - 1 by XREAL_1:9;
then reconsider I = i - 1 as Element of NAT by INT_1:3;
reconsider II = (i + 1) * I as Element of NAT ;
(i ^2) mod (i + 1) = (II + 1) mod (i + 1)
.= ((II mod (i + 1)) + 1) mod (i + 1) by NAT_D:22
.= (0 + 1) mod (i + 1) by NAT_D:13
.= 1 by A2, NAT_D:24 ;
hence (i ^2) mod (i + 1) = 1 ; :: thesis: verum