let i, m, n be Nat; ( n > 1 & m > 1 & m,n are_coprime & i,m * n are_coprime implies order (i,(m * n)) = (order (i,m)) lcm (order (i,n)) )
assume A1:
( n > 1 & m > 1 & m,n are_coprime & i,m * n are_coprime )
; order (i,(m * n)) = (order (i,m)) lcm (order (i,n))
then A2:
m * n > 1 * 1
by XREAL_1:98;
then
i <> 0
by A1, Th5;
then A3:
i > 0
;
set K = (order (i,m)) lcm (order (i,n));
A4:
( m divides m * n & n divides m * n )
by NAT_D:def 3;
then
( order (i,m) divides order (i,(m * n)) & order (i,n) divides order (i,(m * n)) )
by A1, A2, Th20;
then A5:
(order (i,m)) lcm (order (i,n)) divides order (i,(m * n))
by NAT_D:def 4;
i gcd (m * n) = 1
by A1, INT_2:def 3;
then
( i gcd m = 1 & i gcd n = 1 )
by A4, WSIERP_1:16;
then A6:
( i,m are_coprime & i,n are_coprime )
by INT_2:def 3;
(i |^ ((order (i,m)) lcm (order (i,n)))) - 1 >= 0
by NAT_1:14, XREAL_1:48, A3;
then A7:
(i |^ ((order (i,m)) lcm (order (i,n)))) - 1 is Element of NAT
by INT_1:3;
( order (i,m) divides (order (i,m)) lcm (order (i,n)) & order (i,n) divides (order (i,m)) lcm (order (i,n)) )
by NAT_D:def 4;
then
( (i |^ ((order (i,m)) lcm (order (i,n)))) mod m = 1 & (i |^ ((order (i,m)) lcm (order (i,n)))) mod n = 1 )
by A1, A6, PEPIN:48;
then
( i |^ ((order (i,m)) lcm (order (i,n))),1 are_congruent_mod m & i |^ ((order (i,m)) lcm (order (i,n))),1 are_congruent_mod n )
by A1, PEPIN:39;
then
( m divides (i |^ ((order (i,m)) lcm (order (i,n)))) - 1 & n divides (i |^ ((order (i,m)) lcm (order (i,n)))) - 1 )
by INT_2:15;
then
m * n divides (i |^ ((order (i,m)) lcm (order (i,n)))) - 1
by A1, A7, PEPIN:4;
then
i |^ ((order (i,m)) lcm (order (i,n))),1 are_congruent_mod m * n
by INT_2:15;
then A8:
(i |^ ((order (i,m)) lcm (order (i,n)))) mod (m * n) = 1
by A2, PEPIN:39;
order (i,(m * n)) divides (order (i,m)) lcm (order (i,n))
by A1, A2, A8, PEPIN:47;
hence
order (i,(m * n)) = (order (i,m)) lcm (order (i,n))
by A5, NAT_D:5; verum