let G be commutative Group; :: thesis: for a, b being Element of G
for n, m being natural number 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 natural number st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
let n, m be natural number ; :: thesis: ( G is finite & ord a = n & ord b = m & n gcd m = 1 implies ord (a * b) = n * m )
assume A1: ( G is finite & ord a = n & ord b = m & n gcd m = 1 ) ; :: thesis: ord (a * b) = n * m
reconsider n1 = n, m1 = m as Integer ;
( not a is being_of_order_0 & not b is being_of_order_0 ) by A1, GR_CY_1:26;
then A2: ( n <> 0 & m <> 0 ) by A1, GROUP_1:def 12;
then A3: n * m <> 0 by XCMPLX_1:6;
A4: not a * b is being_of_order_0 by A1, GR_CY_1:26;
A5: ( n1,m1 are_relative_prime & m1,n1 are_relative_prime ) by A1, INT_2:def 4;
A6: (a * b) |^ (n * m) = (a |^ (n * m)) * (b |^ (n * m)) by GROUP_1:95
.= ((a |^ n) |^ m) * (b |^ (n * m)) by GROUP_1:50
.= ((a |^ n) |^ m) * ((b |^ m) |^ n) by GROUP_1:50
.= ((1_ G) |^ m) * ((b |^ m) |^ n) by A1, GROUP_1:82
.= ((1_ G) |^ m) * ((1_ G) |^ n) by A1, GROUP_1:82
.= (1_ G) * ((1_ G) |^ n) by GROUP_1:42
.= (1_ G) * (1_ G) by GROUP_1:42
.= 1_ G by GROUP_1:def 5 ;
A7: m * n is Element of NAT by ORDINAL1:def 13;

A8: now

let k be Nat; :: thesis: ( (a * b) |^ k = 1_ G & k <> 0 implies m * n <= k )
assume A9: ( (a * b) |^ k = 1_ G & k <> 0 ) ; :: thesis: m * n <= k
reconsider k1 = k as Integer ;
1_ G = (1_ G) |^ n by GROUP_1:42
.= (a * b) |^ (k * n) by A9, GROUP_1:50
.= (a |^ (k * n)) * (b |^ (k * n)) by GROUP_1:95
.= ((a |^ n) |^ k) * (b |^ (k * n)) by GROUP_1:50
.= ((1_ G) |^ k) * (b |^ (k * n)) by A1, GROUP_1:82
.= (1_ G) * (b |^ (k * n)) by GROUP_1:42
.= b |^ (k * n) by GROUP_1:def 5 ;
then A10: m1 divides k1 by A1, A5, GROUP_1:86, INT_2:40;
1_ G = (1_ G) |^ m by GROUP_1:42
.= (a * b) |^ (k * m) by A9, GROUP_1:50
.= (a |^ (k * m)) * (b |^ (k * m)) by GROUP_1:95
.= (a |^ (k * m)) * ((b |^ m) |^ k) by GROUP_1:50
.= (a |^ (k * m)) * ((1_ G) |^ k) by A1, GROUP_1:82
.= (a |^ (k * m)) * (1_ G) by GROUP_1:42
.= a |^ (k * m) by GROUP_1:def 5 ;
then A11: n1 divides k1 by A1, A5, GROUP_1:86, INT_2:40;
consider i being Integer such that
A12: k1 = m1 * i by A10, INT_1:def 9;
n1 divides i by A5, A11, A12, INT_2:40;
then consider j being Integer such that
A13: i = n1 * j by INT_1:def 9;
A14: k1 = (m1 * n1) * j by A12, A13;
k / (m * n) = j by A2, A14, XCMPLX_1:6, XCMPLX_1:90;
then A15: j is Element of NAT by INT_1:16;
j <> 0 by A9, A12, A13;
then (m * n) * 1 <= (m * n) * j by A15, NAT_1:14, XREAL_1:66;
hence m * n <= k by A12, A13; :: thesis: verum

end;

thus ord (a * b) = n * m by A3, A4, A6, A7, A8, GROUP_1:def 12; :: thesis: verum