let i, m, n be Nat; :: thesis: ( n > 1 & m > 1 & i,n are_coprime & m divides n implies order (i,m) divides order (i,n) )
assume A1: ( n > 1 & m > 1 & i,n are_coprime & m divides n ) ; :: thesis: order (i,m) divides order (i,n)
i gcd n = 1 by A1, INT_2:def 3;
then i gcd m = 1 by A1, WSIERP_1:16;
then A2: i,m are_coprime by INT_2:def 3;
(i |^ (order (i,n))) mod n = 1 by A1, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then i |^ (order (i,n)),1 are_congruent_mod n by A1, NAT_D:64;
then n divides (i |^ (order (i,n))) - 1 by INT_2:15;
then m divides (i |^ (order (i,n))) - 1 by A1, INT_2:9;
then i |^ (order (i,n)),1 are_congruent_mod m by INT_2:15;
then (i |^ (order (i,n))) mod m = 1 mod m by NAT_D:64
.= 1 by A1, PEPIN:5 ;
hence order (i,m) divides order (i,n) by A1, A2, PEPIN:47; :: thesis: verum