let b be non zero Nat; :: thesis: for a being non trivial Nat holds
( a divides b iff a |-count (a gcd b) = 1 )
let a be non trivial Nat; :: thesis: ( a divides b iff a |-count (a gcd b) = 1 )
reconsider c = a gcd b as non zero Nat ;
A1: a > 1 by Def0;
A2: c divides b by INT_2:def 2;
thus ( a divides b implies a |-count (a gcd b) = 1 ) :: thesis: ( a |-count (a gcd b) = 1 implies a divides b )
proof
assume a divides b ; :: thesis: a |-count (a gcd b) = 1
then a gcd b = |.a.| by NEWTON02:3;
hence a |-count (a gcd b) = 1 by NAT_3:22, Def0; :: thesis: verum
end;
assume a |-count (a gcd b) = 1 ; :: thesis: a divides b
then a |^ 1 divides c by A1, NAT_3:def 7;
hence a divides b by A2, INT_2:9; :: thesis: verum