let V be Z_Module; for v being Vector of V st not v is torsion holds
not Lin {v} is divisible
let v be Vector of V; ( not v is torsion implies not Lin {v} is divisible )
assume A1:
not v is torsion
; not Lin {v} is divisible
reconsider i2 = 2 as Element of INT.Ring by INT_1:def 2;
assume A2:
Lin {v} is divisible
; contradiction
v in Lin {v}
by ZMODUL06:20;
then reconsider vv = v as Vector of (Lin {v}) ;
vv is divisible
by A2;
then consider uu being Vector of (Lin {v}) such that
A3:
i2 * uu = vv
;
reconsider u = uu as Vector of V by ZMODUL01:25;
u in Lin {v}
;
then consider i being Element of INT.Ring such that
A4:
u = i * v
by ZMODUL06:19;
reconsider i3 = i as Integer ;
v =
i2 * (i * v)
by A3, A4, ZMODUL01:29
.=
(i2 * i) * v
by VECTSP_1:def 16
;
then
((i2 * i) * v) - v = 0. V
by RLVECT_1:15;
then
((i2 * i) * v) - ((1. INT.Ring) * v) = 0. V
by VECTSP_1:def 17;
then A5:
((i2 * i) - (1. INT.Ring)) * v = 0. V
by ZMODUL01:9;
(2 * i3) - 1 <> 0
hence
contradiction
by A1, A5; verum