let s, t, i, n be Nat; :: thesis: ( n > 1 & i,n are_coprime implies ( i |^ s,i |^ t are_congruent_mod n iff s,t are_congruent_mod order (i,n) ) )
assume A1: ( n > 1 & i,n are_coprime ) ; :: thesis: ( i |^ s,i |^ t are_congruent_mod n iff s,t are_congruent_mod order (i,n) )
A2: ( i <> 0 & n > 0 ) by A1, Th5;
set R = order (i,n);
reconsider RR = order (i,n) as Element of NAT ;
thus ( i |^ s,i |^ t are_congruent_mod n implies s,t are_congruent_mod order (i,n) ) :: thesis: ( s,t are_congruent_mod order (i,n) implies i |^ s,i |^ t are_congruent_mod n )

proof

assume A3: i |^ s,i |^ t are_congruent_mod n ; :: thesis: s,t are_congruent_mod order (i,n)
A4: i gcd n = 1 by A1, INT_2:def 3;

per cases ( s = t or s > t or s < t ) by XXREAL_0:1;

suppose s = t ; :: thesis: s,t are_congruent_mod order (i,n)

hence s,t are_congruent_mod order (i,n) by INT_1:11; :: thesis: verum

end;

suppose s > t ; :: thesis: s,t are_congruent_mod order (i,n)

then consider l being Nat such that
A5: s = t + l by NAT_1:10;
n divides (i |^ s) - (i |^ t) by A3, INT_2:15;
then n divides ((i |^ t) * (i |^ l)) - ((i |^ t) * 1) by A5, NEWTON:8;
then A6: n divides (i |^ t) * ((i |^ l) - 1) ;
reconsider ll = (i |^ l) - 1 as Element of NAT by NAT_1:21, NAT_1:14, A2;
A7: n gcd (i |^ t) = 1 by A4, A2, NAT_4:10;
n divides ll by A6, A7, WSIERP_1:30;
then i |^ l,1 are_congruent_mod n by INT_2:15;
then (i |^ l) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
then order (i,n) divides s - t by A5, A1, PEPIN:47;
hence s,t are_congruent_mod order (i,n) by INT_2:15; :: thesis: verum

end;

suppose s < t ; :: thesis: s,t are_congruent_mod order (i,n)

then consider l being Nat such that
A8: t = s + l by NAT_1:10;
i |^ t,i |^ s are_congruent_mod n by A3, INT_1:14;
then n divides (i |^ t) - (i |^ s) by INT_2:15;
then n divides ((i |^ s) * (i |^ l)) - ((i |^ s) * 1) by A8, NEWTON:8;
then A9: n divides (i |^ s) * ((i |^ l) - 1) ;
A10: n gcd (i |^ s) = 1 by A4, A2, NAT_4:10;
reconsider ll = (i |^ l) - 1 as Element of NAT by NAT_1:21, NAT_1:14, A2;
n divides ll by A10, A9, WSIERP_1:30;
then i |^ l,1 are_congruent_mod n by INT_2:15;
then (i |^ l) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
then order (i,n) divides t - s by A1, A8, PEPIN:47;
then t,s are_congruent_mod order (i,n) by INT_2:15;
hence s,t are_congruent_mod order (i,n) by INT_1:14; :: thesis: verum

end;

end;

end;

assume A11: s,t are_congruent_mod order (i,n) ; :: thesis: i |^ s,i |^ t are_congruent_mod n
A12: order (i,n) > 0 by A1, PEPIN:def 2;
then A13: ( s = ((s div (order (i,n))) * (order (i,n))) + (s mod (order (i,n))) & t = ((t div (order (i,n))) * (order (i,n))) + (t mod (order (i,n))) ) by NEWTON:66;
then A14: i |^ s = (i |^ ((order (i,n)) * (s div (order (i,n))))) * (i |^ (s mod (order (i,n)))) by NEWTON:8
.= ((i |^ (order (i,n))) |^ (s div (order (i,n)))) * (i |^ (s mod (order (i,n)))) by NEWTON:9 ;
A15: (i |^ (order (i,n))) mod n = 1 by A1, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then ((i |^ (order (i,n))) |^ (s div (order (i,n)))) mod n = (1 |^ (s div (order (i,n)))) mod n by INT_4:8
.= 1 mod n ;
then (i |^ (order (i,n))) |^ (s div (order (i,n))),1 are_congruent_mod n by A1, NAT_D:64;
then ((i |^ (order (i,n))) |^ (s div (order (i,n)))) * (i |^ (s mod (order (i,n)))),1 * (i |^ (s mod (order (i,n)))) are_congruent_mod n by INT_4:11;
then A16: (i |^ s) mod n = (i |^ (s mod (order (i,n)))) mod n by A14, NAT_D:64;
A17: i |^ t = (i |^ ((order (i,n)) * (t div (order (i,n))))) * (i |^ (t mod (order (i,n)))) by NEWTON:8, A13
.= ((i |^ (order (i,n))) |^ (t div (order (i,n)))) * (i |^ (t mod (order (i,n)))) by NEWTON:9 ;
((i |^ (order (i,n))) |^ (t div (order (i,n)))) mod n = (1 |^ (t div (order (i,n)))) mod n by A15, INT_4:8
.= 1 mod n ;
then (i |^ (order (i,n))) |^ (t div (order (i,n))),1 are_congruent_mod n by A1, NAT_D:64;
then ((i |^ (order (i,n))) |^ (t div (order (i,n)))) * (i |^ (t mod (order (i,n)))),1 * (i |^ (t mod (order (i,n)))) are_congruent_mod n by INT_4:11;
then A18: (i |^ t) mod n = (i |^ (t mod (order (i,n)))) mod n by A17, NAT_D:64;
( s mod (order (i,n)) = (s mod (order (i,n))) mod (order (i,n)) & t mod (order (i,n)) = (t mod (order (i,n))) mod (order (i,n)) ) by NAT_D:73;
then A19: ( s,s mod (order (i,n)) are_congruent_mod order (i,n) & t,t mod (order (i,n)) are_congruent_mod order (i,n) ) by A12, NAT_D:64;
then t,s mod (order (i,n)) are_congruent_mod order (i,n) by A11, PEPIN:40;
then s mod (order (i,n)),t mod (order (i,n)) are_congruent_mod order (i,n) by A19, PEPIN:40;
then A20: order (i,n) divides (s mod (order (i,n))) - (t mod (order (i,n))) by INT_2:15;

now :: thesis: not s mod (order (i,n)) <> t mod (order (i,n))

assume s mod (order (i,n)) <> t mod (order (i,n)) ; :: thesis: contradiction
then (s mod (order (i,n))) - (t mod (order (i,n))) <> 0 ;
then |.(order (i,n)).| <= |.((s mod (order (i,n))) - (t mod (order (i,n)))).| by A20, INT_4:6;
then A21: order (i,n) <= |.((s mod (order (i,n))) - (t mod (order (i,n)))).| by ABSVALUE:def 1;
reconsider sR = s mod RR, tR = t mod RR as Element of REAL by XREAL_0:def 1;
reconsider rR = - (order (i,n)) as Element of REAL by XREAL_0:def 1;
A22: ( sR < RR & sR >= 0 & tR < RR & tR >= 0 ) by A12, NAT_D:1;
sR - tR <= sR by XREAL_1:43;
then A23: sR - tR < RR by A22, XXREAL_0:2;
A24: (- 1) * tR > (- 1) * RR by XREAL_1:69, A22;
sR + (- tR) >= - tR by XREAL_1:31;
then sR + (- tR) > rR by XXREAL_0:2, A24;
hence contradiction by A21, SEQ_2:1, A23; :: thesis: verum

end;

hence i |^ s,i |^ t are_congruent_mod n by A1, A16, A18, NAT_D:64; :: thesis: verum