let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v))
let v be Valuation of K; ( K is having_valuation implies for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v)) )
assume A1:
K is having_valuation
; for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v))
let x be Element of K; ( x <> 0. K implies ex i being Integer st v . x = i * (least-positive (rng v)) )
assume A2:
x <> 0. K
; ex i being Integer st v . x = i * (least-positive (rng v))
reconsider vx = v . x as Element of INT by A1, A2, Def8;
reconsider l = least-positive (rng v) as Integer by A1, Th35;
A3:
v . x = ((vx div l) * l) + (vx mod l)
by INT_1:59;
per cases
( vx mod l = 0 or vx mod l <> 0 )
;
suppose A5:
vx mod l <> 0
;
ex i being Integer st v . x = i * (least-positive (rng v))consider k being
Element of
K such that A6:
l = v . k
by A1, Lm5, FUNCT_2:113;
set d =
vx div l;
set kd =
k |^ (vx div l);
set kD =
(k |^ (vx div l)) " ;
A7:
k <> 0. K
by A1, A6, Def8;
then A8:
(vx div l) * (v . k) = v . (k |^ (vx div l))
by A1, Th29;
A9:
- (v . (k |^ (vx div l))) = v . ((k |^ (vx div l)) ")
by A1, A7, Th16, Th21;
A10:
(vx div l) * l = (vx div l) * (v . k)
by A6, XXREAL_3:def 5;
A11:
v . (x * ((k |^ (vx div l)) ")) =
(v . x) - ((vx div l) * l)
by A8, A9, A10, A1, Def8
.=
vx - ((vx div l) * l)
by Lm1
.=
vx mod l
by A3
;
then A12:
0 <= v . (x * ((k |^ (vx div l)) "))
by INT_1:57;
A13:
v . (x * ((k |^ (vx div l)) ")) < l
by A11, INT_1:58;
v . (x * ((k |^ (vx div l)) ")) in rng v
by FUNCT_2:4;
hence
ex
i being
Integer st
v . x = i * (least-positive (rng v))
by A12, A5, A11, A13, Def2;
verum end;