hereby :: thesis: ( ( for p being prime Nat holds
( not p divides m or not p divides n ) ) implies m,n are_coprime )
assume A1: m,n are_coprime ; :: thesis: for p being prime Nat st p divides m holds
not p divides n
let p be prime Nat; :: thesis: ( p divides m implies not p divides n )
assume ( p divides m & p divides n ) ; :: thesis: contradiction
then p = 1 by A1;
hence contradiction by INT_2:def 4; :: thesis: verum
end;
assume A2: for p being prime Nat holds
( not p divides m or not p divides n ) ; :: thesis: m,n are_coprime
let k be Nat; :: according to PYTHTRIP:def 1 :: thesis: ( k divides m & k divides n implies k = 1 )
assume A3: ( k divides m & k divides n ) ; :: thesis: k = 1
per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose k = 0 ; :: thesis: k = 1
then ( m = 0 & n = 0 ) by A3;
hence k = 1 by A2, INT_2:28, NAT_D:6; :: thesis: verum
end;
suppose k = 1 ; :: thesis: k = 1
hence k = 1 ; :: thesis: verum
end;
suppose k > 1 ; :: thesis: k = 1
then k >= 1 + 1 by NAT_1:13;
then consider p being Element of NAT such that
A4: p is prime and
A5: p divides k by INT_2:31;
reconsider p9 = p as prime Element of NAT by A4;
( p9 divides m & p9 divides n ) by A3, A5, NAT_D:4;
hence k = 1 by A2; :: thesis: verum
end;
end;