let s, i, n be Nat; ( n > 1 & i,n are_coprime implies ( order (i,n),s are_coprime iff order ((i |^ s),n) = order (i,n) ) )
assume A1:
( n > 1 & i,n are_coprime )
; ( order (i,n),s are_coprime iff order ((i |^ s),n) = order (i,n) )
thus
( order (i,n),s are_coprime implies order ((i |^ s),n) = order (i,n) )
( order ((i |^ s),n) = order (i,n) implies order (i,n),s are_coprime )proof
assume
order (
i,
n),
s are_coprime
;
order ((i |^ s),n) = order (i,n)
then
(order (i,n)) gcd s = 1
by INT_2:def 3;
then
(order (i,n)) div ((order (i,n)) gcd s) = order (
i,
n)
by NAT_2:4;
hence
order (
(i |^ s),
n)
= order (
i,
n)
by A1, Th14;
verum
end;
assume
order ((i |^ s),n) = order (i,n)
; order (i,n),s are_coprime
then A2:
(order (i,n)) div ((order (i,n)) gcd s) = order (i,n)
by A1, Th14;
set d = (order (i,n)) gcd s;
A3:
(order (i,n)) gcd s divides order (i,n)
by NAT_D:def 5;
then A4:
((order (i,n)) div ((order (i,n)) gcd s)) * 1 = ((order (i,n)) div ((order (i,n)) gcd s)) * ((order (i,n)) gcd s)
by A2, NAT_D:3;
A5:
order (i,n) > 0
by A1, PEPIN:def 2;
then A6:
(order (i,n)) gcd s <= order (i,n)
by A3, NAT_D:7;
(order (i,n)) gcd s <> 0
by A5, INT_2:5;
then
(order (i,n)) div ((order (i,n)) gcd s) <> 0
by A6, NAT_2:13;
then
(order (i,n)) gcd s = 1
by A4, XCMPLX_1:5;
hence
order (i,n),s are_coprime
by INT_2:def 3; verum