let s, i, n be Nat; :: thesis: ( n > 1 & i,n are_coprime implies ( i |^ s,1 are_congruent_mod n iff order (i,n) divides s ) )
assume A1: ( n > 1 & i,n are_coprime ) ; :: thesis: ( i |^ s,1 are_congruent_mod n iff order (i,n) divides s )
thus ( i |^ s,1 are_congruent_mod n implies order (i,n) divides s ) :: thesis: ( order (i,n) divides s implies i |^ s,1 are_congruent_mod n )
proof
assume i |^ s,1 are_congruent_mod n ; :: thesis: order (i,n) divides s
then i |^ s,i |^ 0 are_congruent_mod n by NEWTON:4;
then s, 0 are_congruent_mod order (i,n) by A1, Th10;
then order (i,n) divides s - 0 by INT_2:15;
hence order (i,n) divides s ; :: thesis: verum
end;
assume order (i,n) divides s ; :: thesis: i |^ s,1 are_congruent_mod n
then order (i,n) divides s - 0 ;
then s, 0 are_congruent_mod order (i,n) by INT_2:15;
then i |^ s,i |^ 0 are_congruent_mod n by A1, Th10;
hence i |^ s,1 are_congruent_mod n by NEWTON:4; :: thesis: verum