let i, n be Nat; :: thesis: ( n > 1 & i,n are_coprime implies i <> 0 )
assume A1: ( n > 1 & i,n are_coprime ) ; :: thesis: i <> 0
assume i = 0 ; :: thesis: contradiction
then i gcd n > 1 by A1, NEWTON:52;
hence contradiction by A1, INT_2:def 3; :: thesis: verum