let V be non trivial torsion finitely-generated Z_Module; :: thesis: for i being Element of INT.Ring st i <> 0 & ( for v being Vector of V holds i * v = 0. V ) holds
not V is divisible
let i be Element of INT.Ring; :: thesis: ( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) implies not V is divisible )
assume A1: ( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) ) ; :: thesis: not V is divisible
assume AS: V is divisible ; :: thesis: contradiction
set v = the non zero Vector of V;
the non zero Vector of V is divisible by AS;
then consider u being Vector of V such that
A2: i * u = the non zero Vector of V by A1;
thus contradiction by A1, A2; :: thesis: verum