let s, t, n be Nat; :: thesis:
assume A1: ( n > 1 & s,n are_coprime & t,n are_coprime & order ((s * t),n) = (order (s,n)) * (order (t,n)) ) ; :: thesis:
then ( s gcd n = 1 & t gcd n = 1 ) by INT_2:def 3;
then (s * t) gcd n = 1 by WSIERP_1:7;
then A2: s * t,n are_coprime by INT_2:def 3;
set L = (order (s,n)) lcm (order (t,n));
( order (s,n) > 0 & order (t,n) > 0 ) by A1, PEPIN:def 2;
then A3: (order (s,n)) lcm (order (t,n)) <> 0 by INT_2:4;
( order (s,n) divides order ((s * t),n) & order (t,n) divides order ((s * t),n) ) by A1, NAT_D:def 3;
then A4: (order (s,n)) lcm (order (t,n)) divides order ((s * t),n) by NAT_D:def 4;
A5: ( order (s,n) divides (order (s,n)) lcm (order (t,n)) & order (t,n) divides (order (s,n)) lcm (order (t,n)) ) by NAT_D:def 4;
then (s |^ ((order (s,n)) lcm (order (t,n)))) mod n = 1 by A1, PEPIN:48
.= 1 mod n by A1, PEPIN:5 ;
then A6: s |^ ((order (s,n)) lcm (order (t,n))),1 are_congruent_mod n by A1, NAT_D:64;
(t |^ ((order (s,n)) lcm (order (t,n)))) mod n = 1 by A1, A5, PEPIN:48
.= 1 mod n by A1, PEPIN:5 ;
then t |^ ((order (s,n)) lcm (order (t,n))),1 are_congruent_mod n by A1, NAT_D:64;
then A7: (t |^ ((order (s,n)) lcm (order (t,n)))) * (s |^ ((order (s,n)) lcm (order (t,n)))),1 * 1 are_congruent_mod n by A6, INT_1:18;
set B = s * t;
(s * t) |^ ((order (s,n)) lcm (order (t,n))),1 * 1 are_congruent_mod n by A7, NEWTON:7;
then A8: ((s * t) |^ ((order (s,n)) lcm (order (t,n)))) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
order ((s * t),n) divides (order (s,n)) lcm (order (t,n)) by A8, A1, A2, PEPIN:47;
then (order (s,n)) lcm (order (t,n)) = (order (s,n)) * (order (t,n)) by A1, A4, NAT_D:5;
then ((order (s,n)) lcm (order (t,n))) * ((order (s,n)) gcd (order (t,n))) = ((order (s,n)) lcm (order (t,n))) * 1 by NAT_D:29;
then (order (s,n)) gcd (order (t,n)) = 1 by A3, XCMPLX_1:5;
hence order (s,n), order (t,n) are_coprime by INT_2:def 3; :: thesis: