let G be commutative Group; :: thesis: for a, b being Element of G
for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
let a, b be Element of G; :: thesis: for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
let n, m be Nat; :: thesis: ( G is finite & ord a = n & ord b = m & n gcd m = 1 implies ord (a * b) = n * m )
assume that
A1: G is finite and
A2: ord a = n and
A3: ord b = m and
A4: n gcd m = 1 ; :: thesis: ord (a * b) = n * m
not b is being_of_order_0 by A1, GR_CY_1:6;
then A5: m <> 0 by A3, GROUP_1:def 11;
A6: not a * b is being_of_order_0 by A1, GR_CY_1:6;
A7: (a * b) |^ (n * m) = (a |^ (n * m)) * (b |^ (n * m)) by GROUP_1:48
.= ((a |^ n) |^ m) * (b |^ (n * m)) by GROUP_1:35
.= ((a |^ n) |^ m) * ((b |^ m) |^ n) by GROUP_1:35
.= ((1_ G) |^ m) * ((b |^ m) |^ n) by A2, GROUP_1:41
.= ((1_ G) |^ m) * ((1_ G) |^ n) by A3, GROUP_1:41
.= (1_ G) * ((1_ G) |^ n) by GROUP_1:31
.= (1_ G) * (1_ G) by GROUP_1:31
.= 1_ G by GROUP_1:def 4 ;
A8: m * n is Element of NAT by ORDINAL1:def 12;
reconsider n1 = n, m1 = m as Integer ;
A9: n1,m1 are_coprime by A4, INT_2:def 3;
not a is being_of_order_0 by A1, GR_CY_1:6;
then A10: n <> 0 by A2, GROUP_1:def 11;

A11: now :: thesis: for k being Nat st (a * b) |^ k = 1_ G & k <> 0 holds
m * n <= k

let k be Nat; :: thesis: ( (a * b) |^ k = 1_ G & k <> 0 implies m * n <= k )
assume that
A12: (a * b) |^ k = 1_ G and
A13: k <> 0 ; :: thesis: m * n <= k
reconsider k1 = k as Integer ;
1_ G = (1_ G) |^ n by GROUP_1:31
.= (a * b) |^ (k * n) by A12, GROUP_1:35
.= (a |^ (k * n)) * (b |^ (k * n)) by GROUP_1:48
.= ((a |^ n) |^ k) * (b |^ (k * n)) by GROUP_1:35
.= ((1_ G) |^ k) * (b |^ (k * n)) by A2, GROUP_1:41
.= (1_ G) * (b |^ (k * n)) by GROUP_1:31
.= b |^ (k * n) by GROUP_1:def 4 ;
then m1 divides k1 by A3, A9, GROUP_1:44, INT_2:25;
then consider i being Integer such that
A14: k1 = m1 * i by INT_1:def 3;
1_ G = (1_ G) |^ m by GROUP_1:31
.= (a * b) |^ (k * m) by A12, GROUP_1:35
.= (a |^ (k * m)) * (b |^ (k * m)) by GROUP_1:48
.= (a |^ (k * m)) * ((b |^ m) |^ k) by GROUP_1:35
.= (a |^ (k * m)) * ((1_ G) |^ k) by A3, GROUP_1:41
.= (a |^ (k * m)) * (1_ G) by GROUP_1:31
.= a |^ (k * m) by GROUP_1:def 4 ;
then n1 divides k1 by A2, A9, GROUP_1:44, INT_2:25;
then n1 divides i by A9, A14, INT_2:25;
then consider j being Integer such that
A15: i = n1 * j by INT_1:def 3;
k1 = (m1 * n1) * j by A14, A15;
then k / (m * n) = j by A10, A5, XCMPLX_1:6, XCMPLX_1:89;
then A16: j is Element of NAT by INT_1:3;
j <> 0 by A13, A14, A15;
then (m * n) * 1 <= (m * n) * j by A16, NAT_1:14, XREAL_1:64;
hence m * n <= k by A14, A15; :: thesis: verum

end;

n * m <> 0 by A10, A5, XCMPLX_1:6;
hence ord (a * b) = n * m by A6, A7, A8, A11, GROUP_1:def 11; :: thesis: verum