let V be non trivial free Z_Module; :: thesis: for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st
( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
let v be Vector of (DivisibleMod V); :: thesis: ex a being Element of INT.Ring st
( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
consider ai being Element of INT.Ring such that
A2: ( ai <> 0 & ai * v in EMbedding V ) by ThDM1;
reconsider aiv = ai * v as Vector of (EMbedding V) by A2;
A3: |.ai.| * v in EMbedding V

proof

B1: EMbedding V is Submodule of DivisibleMod V by ThDivisible2;

per cases ( ai > 0 or ai < 0 ) by A2;

suppose ai > 0 ; :: thesis: |.ai.| * v in EMbedding V

hence |.ai.| * v in EMbedding V by A2, ABSVALUE:def 1; :: thesis: verum

end;

suppose ai < 0 ; :: thesis: |.ai.| * v in EMbedding V

then |.ai.| * v = (- ai) * v by ABSVALUE:def 1
.= - (ai * v) by ZMODUL01:16
.= - aiv by B1, ZMODUL01:30 ;
hence |.ai.| * v in EMbedding V ; :: thesis: verum

end;

end;

end;

reconsider ain = |.ai.| as Element of INT.Ring ;
reconsider ainv = ain * v as Vector of (EMbedding V) by A3;
N1: |.ai.| in NAT by COMPLEX1:46, INT_1:3;
then reconsider nai = |.ai.| as Nat ;
A4: ain <> 0 by A2, ABSVALUE:2;
defpred S₁[ Nat] means ex n being Element of INT.Ring st
( n = $1 & n in NAT & n <> 0 & n * v in EMbedding V );
A6: ex k being Nat st S₁[k] by A3, A4, N1;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A6);
then consider a0 being Nat such that
A7: ( S₁[a0] & ( for b0 being Nat st S₁[b0] holds
a0 <= b0 ) ) ;
reconsider a = a0 as Element of INT.Ring by INT_1:def 2;
take a ; :: thesis: ( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
thus a in NAT by ORDINAL1:def 12; :: thesis: ( a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
thus a <> 0 by A7; :: thesis: ( a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
thus a * v in EMbedding V by A7; :: thesis: for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V
thus for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V by A7; :: thesis: verum