let a, b be natural Ordinal; :: thesis: ( a,b are_coprime iff a hcf b = 1 )
a hcf b divides b by Def5;
then A1: b = (a hcf b) *^ (b div^ (a hcf b)) by Th7;
a hcf b divides a by Def5;
then a = (a hcf b) *^ (a div^ (a hcf b)) by Th7;
hence ( a,b are_coprime implies a hcf b = 1 ) by A1; :: thesis: ( a hcf b = 1 implies a,b are_coprime )
assume A2: a hcf b = 1 ; :: thesis: a,b are_coprime
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( a = c *^ d1 & b = c *^ d2 implies c = 1 )
assume A3: ( a = c *^ d1 & b = c *^ d2 ) ; :: thesis: c = 1
( a <> {} or b <> {} ) by A2, Th14, Lm4;
then reconsider c = c as Element of omega by A3, ORDINAL3:75;
( c divides a & c divides b ) by A3;
then c divides 1 by A2, Def5;
then ex d being natural Ordinal st 1 = c *^ d by Th5;
hence c = 1 by ORDINAL3:37; :: thesis: verum