let s, t, n be Nat; ( n > 1 & s,n are_coprime & (s * t) mod n = 1 implies order (s,n) = order (t,n) )
assume A1:
( n > 1 & s,n are_coprime & (s * t) mod n = 1 )
; order (s,n) = order (t,n)
set f = t gcd n;
A8:
order (s,n) > 0
by A1, PEPIN:def 2;
set M = s * t;
A9:
(s * t) mod n = 1 mod n
by A1, PEPIN:5;
then ((s * t) |^ (order (s,n))) mod n =
(1 |^ (order (s,n))) mod n
by INT_4:8
.=
1 mod n
.=
1
by A1, PEPIN:5
;
then A10:
((s |^ (order (s,n))) * (t |^ (order (s,n)))) mod n = 1
by NEWTON:7;
(s |^ (order (s,n))) mod n = 1
by A1, PEPIN:def 2;
then A11:
(t |^ (order (s,n))) mod n = 1
by A10, Th6;
for k being Nat st k > 0 & (t |^ k) mod n = 1 holds
( 0 < order (s,n) & order (s,n) <= k )
proof
let k be
Nat;
( k > 0 & (t |^ k) mod n = 1 implies ( 0 < order (s,n) & order (s,n) <= k ) )
assume A12:
(
k > 0 &
(t |^ k) mod n = 1 )
;
( 0 < order (s,n) & order (s,n) <= k )
k is
Element of
NAT
by ORDINAL1:def 12;
then ((s * t) |^ k) mod n =
(1 |^ k) mod n
by A9, INT_4:8
.=
1
mod n
.=
1
by A1, PEPIN:5
;
then
((s |^ k) * (t |^ k)) mod n = 1
by NEWTON:7;
then
(s |^ k) mod n = 1
by A12, Th6;
hence
(
0 < order (
s,
n) &
order (
s,
n)
<= k )
by A1, A12, PEPIN:def 2;
verum
end;
hence
order (s,n) = order (t,n)
by A11, A8, A2, A1, PEPIN:def 2; verum