let a, b be non zero Nat; :: thesis: ( a gcd b = 1 iff for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 )
thus ( a gcd b = 1 implies for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 ) :: thesis: ( ( for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 ) implies a gcd b = 1 )

proof

assume a gcd b = 1 ; :: thesis: for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0
then B1: a,b are_coprime ;
for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0

proof

let c be non trivial Nat; :: thesis: (c |-count a) * (c |-count b) = 0
C1: c <> 1 by Def0;

per cases ( not c divides a or c divides a ) ;

suppose not c divides a ; :: thesis: (c |-count a) * (c |-count b) = 0

then c |-count a = 0 by C1, NAT_3:27;
hence (c |-count a) * (c |-count b) = 0 ; :: thesis: verum

end;

suppose c divides a ; :: thesis: (c |-count a) * (c |-count b) = 0

then not c divides b by C1, B1, PYTHTRIP:def 1;
then c |-count b = 0 by C1, NAT_3:27;
hence (c |-count a) * (c |-count b) = 0 ; :: thesis: verum

end;

end;

end;

hence for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 ; :: thesis: verum

end;

( ( for c being prime Nat holds (c |-count a) * (c |-count b) = 0 ) implies a gcd b = 1 )

proof

assume B1: for c being prime Nat holds (c |-count a) * (c |-count b) = 0 ; :: thesis: a gcd b = 1
for c being prime Nat holds
( not c divides a or not c divides b )

proof

let c be prime Nat; :: thesis: ( not c divides a or not c divides b )
C1: c <> 1 by INT_2:def 4;
(c |-count a) * (c |-count b) = 0 by B1;
then ( c |-count a = 0 or c |-count b = 0 ) ;
hence ( not c divides a or not c divides b ) by C1, NAT_3:27; :: thesis: verum

end;

then a,b are_coprime by PYTHTRIP:def 2;
hence a gcd b = 1 ; :: thesis: verum

end;

hence ( ( for c being non trivial Nat holds (c |-count a) * (c |-count b) = 0 ) implies a gcd b = 1 ) ; :: thesis: verum