let a, b be natural Ordinal; :: thesis: ( ( a <> {} or b <> {} ) implies a div^ (a hcf b),b div^ (a hcf b) are_coprime )
assume A1: ( a <> {} or b <> {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_coprime
set ab = a hcf b;
A2: ( 1 *^ a = a & 1 *^ b = b ) by ORDINAL2:39;
per cases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ;
suppose ( a = {} or b = {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_coprime
then ( ( a hcf b = b & b div^ b = 1 ) or ( a hcf b = a & a div^ a = 1 ) ) by A1, A2, Th14, ORDINAL3:68;
hence a div^ (a hcf b),b div^ (a hcf b) are_coprime by Th2; :: thesis: verum
end;
suppose A3: ( a <> {} & b <> {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_coprime
a hcf b divides b by Def5;
then A4: b = (a hcf b) *^ (b div^ (a hcf b)) by Th7;
then A5: b div^ (a hcf b) <> {} by A3, ORDINAL2:35;
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( a div^ (a hcf b) = c *^ d1 & b div^ (a hcf b) = c *^ d2 implies c = 1 )
assume that
A6: a div^ (a hcf b) = c *^ d1 and
A7: b div^ (a hcf b) = c *^ d2 ; :: thesis: c = 1
a hcf b divides a by Def5;
then A8: a = (a hcf b) *^ (a div^ (a hcf b)) by Th7;
then a div^ (a hcf b) <> {} by A3, ORDINAL2:35;
then reconsider c = c, d1 = d1, d2 = d2 as Element of omega by A6, A7, A5, ORDINAL3:75;
b = ((a hcf b) *^ c) *^ d2 by A4, A7, ORDINAL3:50;
then A9: (a hcf b) *^ c divides b ;
a = ((a hcf b) *^ c) *^ d1 by A8, A6, ORDINAL3:50;
then (a hcf b) *^ c divides a ;
then (a hcf b) *^ c divides a hcf b by A9, Def5;
then a hcf b = ((a hcf b) *^ c) *^ ((a hcf b) div^ ((a hcf b) *^ c)) by Th7;
then a hcf b = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) by ORDINAL3:50;
then A10: (a hcf b) *^ 1 = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) by ORDINAL2:39;
a hcf b <> {} by A3, A8, ORDINAL2:35;
then 1 = c *^ ((a hcf b) div^ ((a hcf b) *^ c)) by A10, ORDINAL3:33;
hence c = 1 by ORDINAL3:37; :: thesis: verum
end;
end;