let s, t, n be Nat; :: thesis: ( n > 1 & s,n are_coprime & t,n are_coprime & order (s,n), order (t,n) are_coprime implies order ((s * t),n) = (order (s,n)) * (order (t,n)) )
assume A1: ( n > 1 & s,n are_coprime & t,n are_coprime & order (s,n), order (t,n) are_coprime ) ; :: thesis: order ((s * t),n) = (order (s,n)) * (order (t,n))
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)) * (order (t,n));
A3: ((s * t) |^ (order ((s * t),n))) mod n = 1 by A1, A2, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then (((s * t) |^ (order ((s * t),n))) |^ (order (s,n))) mod n = (1 |^ (order (s,n))) mod n by INT_4:8;
then ((s * t) |^ ((order ((s * t),n)) * (order (s,n)))) mod n = (1 |^ (order (s,n))) mod n by NEWTON:9
.= 1 mod n
.= 1 by A1, PEPIN:5 ;
then (((s * t) |^ (order (s,n))) |^ (order ((s * t),n))) mod n = 1 by NEWTON:9;
then (((s |^ (order (s,n))) * (t |^ (order (s,n)))) |^ (order ((s * t),n))) mod n = 1 by NEWTON:7;
then A4: (((s |^ (order (s,n))) |^ (order ((s * t),n))) * ((t |^ (order (s,n))) |^ (order ((s * t),n)))) mod n = 1 by NEWTON:7;
(s |^ (order (s,n))) mod n = 1 by A1, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then ((s |^ (order (s,n))) |^ (order ((s * t),n))) mod n = (1 |^ (order ((s * t),n))) mod n by INT_4:8
.= 1 mod n ;
then (s |^ (order (s,n))) |^ (order ((s * t),n)),1 are_congruent_mod n by A1, NAT_D:64;
then ((s |^ (order (s,n))) |^ (order ((s * t),n))) * ((t |^ (order (s,n))) |^ (order ((s * t),n))),1 * ((t |^ (order (s,n))) |^ (order ((s * t),n))) are_congruent_mod n by INT_4:11;
then ((t |^ (order (s,n))) |^ (order ((s * t),n))) mod n = 1 by A4, NAT_D:64;
then A5: (t |^ ((order (s,n)) * (order ((s * t),n)))) mod n = 1 by NEWTON:9;
A6: order (t,n) divides order ((s * t),n) by A1, A5, PEPIN:47, PEPIN:3;
(((s * t) |^ (order ((s * t),n))) |^ (order (t,n))) mod n = (1 |^ (order (t,n))) mod n by A3, INT_4:8;
then ((s * t) |^ ((order ((s * t),n)) * (order (t,n)))) mod n = (1 |^ (order (t,n))) mod n by NEWTON:9
.= 1 mod n
.= 1 by A1, PEPIN:5 ;
then (((s * t) |^ (order (t,n))) |^ (order ((s * t),n))) mod n = 1 by NEWTON:9;
then (((s |^ (order (t,n))) * (t |^ (order (t,n)))) |^ (order ((s * t),n))) mod n = 1 by NEWTON:7;
then A7: (((s |^ (order (t,n))) |^ (order ((s * t),n))) * ((t |^ (order (t,n))) |^ (order ((s * t),n)))) mod n = 1 by NEWTON:7;
(t |^ (order (t,n))) mod n = 1 by A1, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then ((t |^ (order (t,n))) |^ (order ((s * t),n))) mod n = (1 |^ (order ((s * t),n))) mod n by INT_4:8
.= 1 mod n ;
then (t |^ (order (t,n))) |^ (order ((s * t),n)),1 are_congruent_mod n by A1, NAT_D:64;
then ((t |^ (order (t,n))) |^ (order ((s * t),n))) * ((s |^ (order (t,n))) |^ (order ((s * t),n))),1 * ((s |^ (order (t,n))) |^ (order ((s * t),n))) are_congruent_mod n by INT_4:11;
then ((s |^ (order (t,n))) |^ (order ((s * t),n))) mod n = 1 by A7, NAT_D:64;
then (s |^ ((order (t,n)) * (order ((s * t),n)))) mod n = 1 by NEWTON:9;
then order (s,n) divides order ((s * t),n) by A1, PEPIN:3, PEPIN:47;
then A8: (order (s,n)) * (order (t,n)) divides order ((s * t),n) by A6, A1, PEPIN:4;
( order (s,n) divides (order (s,n)) * (order (t,n)) & order (t,n) divides (order (s,n)) * (order (t,n)) ) by NAT_D:def 3;
then ( (s |^ ((order (s,n)) * (order (t,n)))) mod n = 1 & (t |^ ((order (s,n)) * (order (t,n)))) mod n = 1 ) by A1, PEPIN:48;
then ( s |^ ((order (s,n)) * (order (t,n))),1 are_congruent_mod n & t |^ ((order (s,n)) * (order (t,n))),1 are_congruent_mod n ) by A1, PEPIN:39;
then (s |^ ((order (s,n)) * (order (t,n)))) * (t |^ ((order (s,n)) * (order (t,n)))),1 * 1 are_congruent_mod n by INT_1:18;
then (s * t) |^ ((order (s,n)) * (order (t,n))),1 are_congruent_mod n by NEWTON:7;
then ((s * t) |^ ((order (s,n)) * (order (t,n)))) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
then order ((s * t),n) divides (order (s,n)) * (order (t,n)) by A1, A2, PEPIN:47;
hence order ((s * t),n) = (order (s,n)) * (order (t,n)) by A8, NAT_D:5; :: thesis: verum