let V be non trivial free Z_Module; for v being non zero Vector of V ex a being Element of INT.Ring st
( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )
let v be non zero Vector of V; ex a being Element of INT.Ring st
( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )
set I = the Basis of V;
A1:
( the Basis of V is linearly-independent & (Omega). V = Lin the Basis of V )
by VECTSP_7:def 3;
consider L being Linear_Combination of the Basis of V, w being Vector of V such that
A2:
( v = Sum L & w in the Basis of V & L . w <> 0 )
by LmND1;
reconsider a = |.(L . w).| as Element of INT.Ring ;
A3:
for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u
proof
let b be
Element of
INT.Ring;
for u being Vector of V st b > a holds
v <> b * ulet u be
Vector of
V;
( b > a implies v <> b * u )
assume B0:
b > a
;
v <> b * u
assume B1:
v = b * u
;
contradiction
u in Lin the
Basis of
V
by A1;
then consider Lu being
Linear_Combination of the
Basis of
V such that B2:
u = Sum Lu
by ZMODUL02:64;
reconsider Lnu =
b * Lu as
Linear_Combination of the
Basis of
V by ZMODUL02:31;
B4:
Sum Lnu = Sum L
by A2, B1, B2, ZMODUL02:53;
(
Carrier Lnu c= the
Basis of
V &
Carrier L c= the
Basis of
V )
by VECTSP_6:def 4;
then B5:
Lnu = L
by B4, VECTSP_7:def 3, ZMODUL03:3;
B6:
Lnu . w = b * (Lu . w)
by VECTSP_6:def 9;
reconsider ib =
b as
Integer ;
|.(L . w).| <> 0
by A2, ABSVALUE:2;
then B8:
|.(L . w).| > 0
by COMPLEX1:46;
N3:
0 <= b
by B0, COMPLEX1:46;
|.(L . w).| =
|.b.| * |.(Lu . w).|
by B5, B6, COMPLEX1:65
.=
ib * |.(Lu . w).|
by N3, ABSVALUE:def 1
;
hence
contradiction
by B0, B8, INT_1:def 3, INT_2:27;
verum
end;
take
a
; ( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )
thus
( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )
by A3, COMPLEX1:46, INT_1:3; verum